Theorem syl6ibr 213

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

Hypotheses

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

Assertion

Ref	Expression
syl6ibr	|- (ph -> (ps -> th))

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 |- (ph -> (ps -> ch))
2		syl6ibr.2	. . 3 |- (th <-> ch)
3	2	biimpr 152	. 2 |- (ch -> th)
4	1, 3	syl6 22	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  imp4a 364  nicodraw 949  hband 1107  equs5e 1194  mopick2 1429  euor2 1430  2moswap 1437  2eu1 1442  necon3bd 1595  necon3d 1596  necon2ad 1606  r19.21ad 1709  cla4egf 1852  cla42gv 1856  cla43gv 1858  ra5 1990  difsn 2455  pwpw0 2460  sssn 2464  ssuni 2512  dfwe2 2925  wefrc 2933  ordtri3or 2969  ordtri3 2973  ordon 2977  ssorduni 2983  oneqmini 3007  tfis 3117  nnsuc 3138  ssrel 3237  opeldm 3303  relssres 3376  cotr 3420  cnvsym 3421  ssrnres 3467  funss 3520  fnun 3580  f1oun 3691  ssimaex 3753  fvopab3ig 3763  chfnrn 3787  dffo4 3805  dffo5 3806  fvclss 3840  isomin 3884  isofrlem 3886  f1oweALT 3891  rdglim2 3934  tz7.48lem 3940  tz7.49 3944  fnoprabg 3997  oprabvalig 4009  infsdomnn 4511  pssnn 4513  pm54.43 4546  inf3lem4 4588  rankr1 4646  r1pwcl 4659  aceq5lem4 4710  aceq5 4712  aceq6b 4714  ac5b 4725  kmlem2 4738  zorn2lem4 4763  zorn2lem6 4765  zorn2lem7 4766  cardne 4802  carden 4803  carddom 4808  alephordi 4846  cardaleph 4857  carduniima 4862  cardinfima 4863  alephval3 4875  cflim 4881  indpi 5006  ltaddpq 5051  genpcl 5083  prlem934 5111  ltaddpr 5112  ltexprlem1 5114  ltexprlem5 5118  reclem4pr 5131  suplem1pr 5133  pre-axsup 5263  zaddclt 6112  zmulclt 6127  zneo 6147  zneoOLD 6148  uzwo4OLD 6158  icoshft 6341  uzwo 6387  uzwoOLD 6388  nn0opth 6596  sqr2irr 6659  caubnd 6863  bccl2t 6909  iserzcmp0 7079  caucvglem2 7094  basgen2t 7581  distop 7591  cnpco 7708  cncnplem2 7714  metreslem 7762  unirnbl 7815  metelcls 7900  ubthlem5 8464  shmods 9277  orthin 9285  spansneleqOLD 9410  h1datom 9421  osumlem4 9498  stcltr2 10112  atom1d 10188  sumdmdi 10249  cdj3lem1 10266  oprabvaligg 10341  cdrci 10381  fipfil 10438  fipfil2 10439  filintf 10443  rdmob 10525

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