Theorem syl5ib 206

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition.

Hypotheses

Ref	Expression
syl5ib.1	|- (ph -> (ps -> ch))
syl5ib.2	|- (th <-> ps)

Assertion

Ref	Expression
syl5ib	|- (ph -> (th -> ch))

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 |- (ph -> (ps -> ch))
2		syl5ib.2	. . 3 |- (th <-> ps)
3	2	biimp 151	. 2 |- (th -> ps)
4	1, 3	syl5 21	1 |- (ph -> (th -> ch))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  orel2 252  ancomsd 437  pm5.18 660  ccased 756  oplem1 772  3jao 886  19.9t 1035  sbequ2 1179  ax11indn 1366  ax11indi 1367  mo 1393  2mo 1447  necon3ad 1602  necon1ad 1631  r19.23ad 1745  moi2 1924  moi 1925  disjsn 2441  pwpw0 2469  prss 2471  sssn 2473  eqsn 2474  tpss 2476  prel12 2484  pwsnALT 2501  intss1 2548  intmin 2553  iinss 2600  trel3 2688  trin 2690  ssopab2 2822  po3nr 2848  fri 2918  frirr 2924  fr2nr 2925  fr3nr 2926  dfwe2 2935  wefrc 2943  onfr 2986  ssorduni 2993  ord0eln0 3023  onmindif 3060  onmindif2 3061  ordunel 3084  limuni3 3123  tfis2f 3128  tfinds2 3165  tfinds3 3166  brrelex 3207  brelg 3222  ssrel 3247  relop 3275  funopg 3547  funssres 3552  funun 3554  funcnvuni 3564  fv3 3733  fvelima 3764  eqfnfv 3797  funfvop 3803  dff2 3817  dff3 3818  fopab2 3823  fvclss 3855  cbvfo 3885  isomin 3899  isofrlem 3901  f1oweALT 3906  canth 3907  iunon 3909  iinon 3910  tfrlem1 3911  tfr3 3926  oaordi 4180  oawordeulem 4188  oeordi 4214  oaabs 4252  nneob 4255  omsmolem 4256  erdisj 4286  th3qlem1 4314  mapenlem2 4490  mapdom2 4494  phplem4 4511  php3 4515  php3OLD 4516  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  iunfiOLD 4569  suppr 4590  elirrv 4598  suc11reg 4605  trcl 4645  zfregs 4647  rankxplim3 4714  cplem1 4720  karden 4726  aceq3lem 4732  aceq5 4740  aceq6b 4742  ac6lem 4754  zorn2lem4 4791  zorn2lem5 4792  zorn2lem7 4794  brdom6disj 4805  fnrndomg 4807  unidom 4808  carddom 4836  unxpdomlem 4843  alephordi 4874  alephord 4875  alephval2 4902  cfub 4908  ltmpi 5031  ltexpq 5080  ltexprlem2 5143  ltexprlem6 5147  reclem3pr 5158  reclem4pr 5159  suplem1pr 5161  mulgt0sr 5214  ssgt0sr 5217  suppsrlem 5221  suppsr2 5223  suppsr3 5224  supsr 5231  suprelem 5259  axrrecex 5284  pre-axsup 5291  ltlent 5522  nnleltp1t 5954  infmrcl 6069  xrsupexmnf 6074  xrinfmexpnf 6075  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxrre 6083  supxrun 6085  lt0nnn0 6116  nnnn0addclt 6125  elnn0nn 6171  flval3t 6239  ioojoint 6416  fznt 6493  expp1t 6574  expne0it 6588  expge0t 6591  nn0opth 6666  creur 6742  creui 6743  seq1bnd 6910  seq1ublem 6911  cau3i 6914  cau5i 6917  cau4i 6918  cau5 6919  facwordit 6944  faclbnd4lem4 6951  bccl2t 6971  2climnn 7102  2climnn0 7103  climaddlem3 7116  climmullem8 7127  climsup 7155  ser1f0 7170  cvgcmp3cetlem2 7189  ivthlem6 7286  ivthlem7 7287  acdc2 7490  acdc 7495  infxpidmlem7 7558  infxpidmlem8 7559  infxpidmlem12 7563  infdif 7568  unctb 7577  unitgt 7623  tgclt 7624  bastop 7642  subtop 7646  indistop 7648  fctopOLD 7650  cctop 7652  elcls3 7711  cnsscnp 7772  cncnp 7778  cnconst 7780  sncld 7787  opnuni 7868  iscau3 7938  iscau4 7940  xpcn 7976  iscms2lem5 7993  bcthlem8 8006  bcthlem33 8031  ghgrpilem2 8134  nmoubi 8435  lnon0 8458  spwval2 8653  shftefif1olem 8741  chcmh 9113  occllem6 9178  pjtheu 9235  shmods 9362  spanunsn 9502  h1datom 9504  osumlem7 9584  nmopubt 9832  nmfnleubt 9849  stm1r 10171  stadd3 10175  mdsl1 10248  cvmd 10251  superpos 10281  chjatom 10284  irred 10321  atcvat4 10324  sumdmdi 10342  sumdmdlem 10345  cdj3lem2a 10363  cdj3lem3a 10366  cdj3 10368  uninqs 10441  cdrci 10494  bsi 10495  mapudiscn 10512  qusp 10555  oefil2 10567  fisub 10576  fisubOLD 10577  rcfpfillem4 10591  rcfpfillem4OLD 10592  rcfpfillem6 10595  rcfpfillem6OLD 10596

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain