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 950  hband 1109  equs5e 1196  mopick2 1434  euor2 1435  2moswap 1442  2eu1 1447  necon3bd 1600  necon3d 1601  necon2ad 1611  r19.21ad 1714  cla4egf 1857  cla42gv 1861  cla43gv 1863  ra5 1996  difsn 2460  pwpw0 2465  sssn 2469  ssuni 2517  dfwe2 2930  wefrc 2938  ordtri3or 2974  ordtri3 2978  ordon 2982  ssorduni 2988  oneqmini 3012  tfis 3122  nnsuc 3143  ssrel 3242  opeldm 3309  relssres 3384  cotr 3428  cnvsym 3429  ssrnres 3473  funss 3526  fnun 3586  f1oun 3697  ssimaex 3759  fvopab3ig 3769  chfnrn 3793  dffo4 3811  dffo5 3812  fvclss 3846  isomin 3890  isofrlem 3892  f1oweALT 3897  rdglim2 3940  tz7.48lem 3946  tz7.49 3950  fnoprabg 4003  oprabvalig 4015  infsdomnn 4517  pssnn 4519  pm54.43 4552  inf3lem4 4596  rankr1 4654  r1pwcl 4667  aceq5lem4 4718  aceq5 4720  aceq6b 4722  ac5b 4733  kmlem2 4746  zorn2lem4 4771  zorn2lem6 4773  zorn2lem7 4774  cardne 4810  carden 4811  carddom 4816  alephordi 4854  cardaleph 4865  carduniima 4870  cardinfima 4871  alephval3 4883  cflim 4889  indpi 5014  ltaddpq 5059  genpcl 5091  prlem934 5119  ltaddpr 5120  ltexprlem1 5122  ltexprlem5 5126  reclem4pr 5139  suplem1pr 5141  pre-axsup 5271  zaddclt 6120  zmulclt 6135  zneo 6155  zneoOLD 6156  uzwo4OLD 6166  icoshft 6349  uzwo 6395  uzwoOLD 6396  nn0opth 6604  sqr2irr 6667  caubnd 6871  bccl2t 6917  iserzcmp0 7087  caucvglem2 7102  basgen2t 7589  distop 7599  cnpco 7719  cncnplem2 7725  metreslem 7774  unirnbl 7827  metelcls 7916  ubthlem5 8477  shmods 9300  orthin 9308  spansneleqOLD 9433  h1datom 9444  osumlem4 9521  stcltr2 10140  atom1d 10217  sumdmdi 10278  cdj3lem1 10295  oprabvaligg 10377  cdrci 10417  fipfil 10474  fipfil2 10475  filintf 10479  rdmob 10561

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