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 954  hband 1113  equs5e 1200  mopick2 1439  euor2 1440  2moswap 1447  2eu1 1452  necon3bd 1606  necon3d 1607  necon2ad 1617  r19.21ad 1720  cla4egf 1864  cla42gv 1868  cla43gv 1870  ra5 2003  difsn 2468  pwpw0 2473  sssn 2477  pwsnALT 2505  ssuni 2526  dfwe2 2941  wefrc 2949  ordtri3or 2985  ordtri3 2989  ordon 2993  ssorduni 2999  oneqmini 3023  tfis 3133  nnsuc 3154  ssrel 3253  opeldm 3320  relssres 3398  cotr 3442  cnvsym 3443  ssrnres 3487  funss 3540  fnun 3600  f1oun 3712  ssimaex 3774  fvopab3ig 3784  chfnrn 3808  dffo4 3826  dffo5 3827  fvclss 3861  isomin 3905  isofrlem 3907  f1oweALT 3912  rdglim2 3955  tz7.48lem 3961  tz7.49 3965  fnoprabg 4018  oprabvalig 4030  infsdomnn 4541  pssnn 4544  ssfi 4547  pm54.43 4581  inf3lem4 4625  rankr1 4684  r1pwcl 4697  aceq5lem4 4748  aceq5 4750  aceq6b 4752  ac5b 4763  kmlem2 4776  zorn2lem4 4801  zorn2lem6 4803  zorn2lem7 4804  cardne 4840  carden 4841  carddom 4846  alephordi 4885  cardaleph 4896  carduniima 4901  cardinfima 4902  alephval3 4914  cflim 4921  indpi 5046  ltaddpq 5091  genpcl 5123  prlem934 5151  ltaddpr 5152  ltexprlem1 5154  ltexprlem5 5158  reclem4pr 5171  suplem1pr 5173  pre-axsup 5303  zaddclt 6167  zmulclt 6182  zneo 6202  uzwo4OLD 6212  icoshft 6409  uzwo 6456  uzwoOLD 6457  nn0opth 6667  sqr2irr 6730  caubnd 6926  bccl2t 6971  iserzcmp0 7143  caucvglem2 7158  basgen2t 7638  distop 7646  cnpco 7766  cncnplem2 7772  metreslem 7819  unirnbl 7872  metelcls 7962  ubthlem5 8529  shmods 9357  orthin 9365  h1datom 9499  osumlem4 9576  stcltr2 10197  atom1d 10275  sumdmdi 10337  cdj3lem1 10356  oprabvaligg 10435  cdrci 10480  fipfil 10549  fipfil2 10550  filintf 10554  rdmob 10652

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