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 659  ccased 755  oplem1 771  3jao 884  19.9t 1033  sbequ2 1177  ax11indn 1364  ax11indi 1365  mo 1391  2mo 1445  necon3ad 1599  necon1ad 1628  r19.23ad 1742  moi2 1920  moi 1921  disjsn 2437  pwpw0 2465  prss 2467  sssn 2469  eqsn 2470  tpss 2472  prel12 2480  intss1 2543  intmin 2548  iinss 2595  trel3 2683  trin 2685  ssopab2 2817  po3nr 2843  fri 2913  frirr 2919  fr2nr 2920  fr3nr 2921  dfwe2 2930  wefrc 2938  onfr 2981  ssorduni 2988  ord0eln0 3018  onmindif 3055  onmindif2 3056  ordunel 3079  limuni3 3118  tfis2f 3123  tfinds2 3160  tfinds3 3161  brrelex 3202  brelg 3217  ssrel 3242  relop 3270  funopg 3539  funssres 3544  funun 3546  funcnvuni 3556  fv3 3724  fvelima 3755  eqfnfv 3788  funfvop 3794  dff2 3808  dff3 3809  fopab2 3814  fvclss 3846  cbvfo 3876  isomin 3890  isofrlem 3892  f1oweALT 3897  canth 3898  iunon 3900  iinon 3901  tfrlem1 3902  tfr3 3917  oaordi 4170  oawordeulem 4178  oeordi 4204  oaabs 4242  nneob 4245  omsmolem 4246  erdisj 4276  th3qlem1 4304  mapenlem2 4476  mapdom2 4480  phplem4 4497  php3 4501  fiint 4540  fodomfi 4546  iunfi 4549  suppr 4570  elirrv 4578  suc11reg 4585  trcl 4625  zfregs 4627  rankxplim3 4694  cplem1 4700  karden 4706  aceq3lem 4712  aceq5 4720  aceq6b 4722  ac6lem 4734  zorn2lem4 4771  zorn2lem5 4772  zorn2lem7 4774  brdom6disj 4785  fnrndomg 4787  unidom 4788  carddom 4816  unxpdomlem 4823  alephordi 4854  alephord 4855  alephval2 4882  cfub 4888  ltmpi 5011  ltexpq 5060  ltexprlem2 5123  ltexprlem6 5127  reclem3pr 5138  reclem4pr 5139  suplem1pr 5141  mulgt0sr 5194  ssgt0sr 5197  suppsrlem 5201  suppsr2 5203  suppsr3 5204  supsr 5211  suprelem 5239  axrrecex 5264  pre-axsup 5271  ltlent 5503  nnleltp1t 5909  infmrcl 6024  xrsupexmnf 6029  xrinfmexpnf 6030  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxrre 6038  supxrun 6040  lt0nnn0 6071  nnnn0addclt 6080  elnn0nn 6126  flval3t 6190  fznt 6433  expp1t 6514  expne0it 6527  expge0t 6530  nn0opth 6604  creur 6681  creui 6682  seq1bnd 6855  seq1ublem 6856  cau3i 6859  cau5i 6862  cau4i 6863  cau5 6864  facwordit 6889  faclbnd4lem4 6896  bccl2t 6917  2climnn 7047  2climnn0 7048  climaddlem3 7060  climmullem8 7071  climsup 7099  ser1f0 7114  cvgcmp3cetlem2 7133  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  acdc2 7440  acdc 7445  infxpidmlem7 7509  infxpidmlem8 7510  infxpidmlem12 7514  infdif 7519  unctb 7527  unitgt 7573  tgclt 7574  bastop 7592  subtop 7596  indistop 7598  fctop 7600  cctop 7602  elcls3 7661  cnsscnp 7722  cncnp 7728  cnconst 7730  sncld 7737  opnuni 7820  iscau3 7890  iscau4 7892  xpcn 7926  iscms2lem5 7943  bcthlem8 7956  bcthlem33 7981  ghgrpilem2 8086  nmoubi 8380  spwval2 8595  shftefif1olem 8680  chcmh 9052  occllem6 9117  pjtheu 9173  shmods 9300  spanunsn 9442  h1datom 9444  osumlem7 9524  nmopubt 9772  nmfnleubt 9788  stm1r 10109  mdsl1 10185  cvmd 10188  superpos 10218  chjatom 10221  irred 10258  atcvat4 10261  sumdmdi 10278  sumdmdlem 10281  cdj3lem2a 10297  cdj3lem3a 10300  cdj3 10302  uninqs 10378  cdrci 10417  bsi 10418  mapudiscn 10435  qusp 10466  oefil2 10477  fisub 10483

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