Theorem syl6bb 252

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
syl6bb	|- (ph -> (ps <-> th))

Proof of Theorem syl6bb

Step	Hyp	Ref	Expression
1		syl6bb.1	. 2 |- (ph -> (ps <-> ch))
2		syl6bb.2	. . 3 |- (ch <-> th)
3	2	a1i 10	. 2 |- (ph -> (ch <-> th))
4	1, 3	bitrd 244	1 |- (ph -> (ps <-> th))

Syntax hints:   -> wi 4   <-> wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  syl6rbb  253  syl6bbr  254  3bitr3g  278  bibi2i  304  ibibr  332  pm5.75  903  cadan  1392  19.17  1861  2eu6  2289  abeq2d  2463  necon2bbid  2575  cbvralf  2830  cbvreu  2834  cbvrab  2858  ceqsralt  2883  ralab2  3002  rexab2  3004  reu7  3032  reu8  3033  2reu5  3045  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  elcomplg  3219  ralss  3333  rexss  3334  prssg  3863  ssunsn2  3866  eqsn  3868  2ralunsn  3881  eluniab  3904  elintab  3938  dfiun2g  4000  dfiin2g  4001  elpw1  4145  eqpw1  4163  pw1in  4165  pw1disj  4168  eluni1g  4173  ssrelk  4212  eqrelk  4213  opkelopkabg  4246  otkelins2kg  4254  otkelins3kg  4255  elimakvg  4259  opkelcokg  4262  elp6  4264  opkelimagekg  4272  dfimak2  4299  eqpw1uni  4331  cbviota  4345  iota1  4354  sniota  4370  dfnnc2  4396  nnsucelr  4429  nndisjeq  4430  ltfinex  4465  ltfintri  4467  ssfin  4471  ncfinlower  4484  evenodddisj  4517  nnadjoin  4521  nnpweq  4524  sfindbl  4531  sfintfin  4533  tfinnn  4535  dfphi2  4570  0cnelphi  4598  proj1op  4601  cbvopab1  4633  setconslem6  4737  opeliunxp  4821  eliunxp  4822  brswap2  4861  elres  4996  xpcan  5058  xpcan2  5059  fncnv  5159  fnres  5200  fun11iun  5306  fnopfvb  5360  funopfvb  5362  fvelrnb  5366  funimass4  5369  fvopab3g  5387  eqfnfv3  5395  eqfnfv2f  5397  fvreseq  5399  inpreima  5410  respreima  5411  fnasrn  5418  fsn  5433  fconstfv  5457  dff13  5472  isocnv  5492  isoini  5498  f1oiso  5500  xpnedisj  5514  funsi  5521  oprabid  5551  eloprabga  5579  resoprab  5582  eqfnov  5590  eqfnov2  5591  ov6g  5601  ovelrn  5609  funimassov  5610  ovelimab  5611  ndmovg  5614  caovord2  5631  cbvmpt  5677  brsnsi  5774  brimage  5794  fntxp  5805  addcfnex  5825  brpprod  5840  fnpprod  5844  pw1fnf1o  5856  clos1ex  5877  erth2  5970  elpmg  6014  elpm2g  6015  xpassenlem  6057  enpw1  6063  enmap2lem3  6066  enprmaplem3  6079  peano4nc  6151  ncspw1eu  6160  ce0addcnnul  6180  nc0suc  6218  taddc  6230  ce0lenc1  6240  muc0or  6253  csucex  6260  addccan2nclem1  6264  nnc3n3p1  6279  nchoicelem12  6301  nchoicelem17  6306  frecxp  6315  fnfreclem3  6320  fnfrec  6321  frecsuc  6323  scancan  6332