Theorem syl6bb 194

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 9	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 186	1 |- ( ph -> ( ps <-> th ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl6rbb  195  syl6bbr  196  3bitr3g  220  bibi2i  225  ibibr  244  imandc  819  pm5.75  903  xordidc  1330  19.17  1488  alexdc  1550  nf4dc  1600  abeq2d  2191  cbvralf  2571  cbvrexf  2572  cbvreu  2575  cbvrab  2599  ceqsralt  2626  ralab2  2756  rexab2  2758  euxfr2dc  2777  reu7  2787  reu8  2788  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  ralss  3060  rexss  3061  prssg  3542  2ralunsn  3590  eluniab  3613  elintab  3647  dfiun2g  3710  dfiin2g  3711  cbvopab1  3851  cbvmpt  3872  axsep2  3897  bnd2  3947  opeqsn  4007  reusv3  4210  tfisi  4328  opeliunxp  4413  eliunxp  4493  relop  4504  eldm2g  4549  reldm0  4571  relrn0  4612  xpmlem  4764  elxp5  4829  cnvpom  4880  cbviota  4892  iota1  4901  sniota  4914  fncnv  4985  fnres  5035  brprcneu  5191  fnopfvb  5236  fvelrnb  5242  fvelimab  5250  fvopab3g  5266  eqfnfv3  5288  eqfnfv2f  5290  fvreseq  5292  fnreseql  5298  rexsupp  5312  respreima  5316  rexrn  5325  ralrn  5326  f1ompt  5341  fsn  5356  fconstfvm  5400  fconst3m  5401  fconst4m  5402  rexima  5415  ralima  5416  dff13  5428  foeqcnvco  5450  fliftfun  5456  isocnv  5471  isoini  5477  f1oiso  5485  cbvriota  5498  eusvobj2  5518  oprabid  5557  eloprabga  5611  resoprab  5617  eqfnov  5627  eqfnov2  5628  ov6g  5658  funimassov  5670  ovelimab  5671  caovord2  5693  releldm2  5831  dfoprab4  5838  xporderlem  5872  poxp  5873  f1od2  5876  mpt2xopovel  5879  brtpos2  5889  brtpos0  5890  rntpos  5895  dftpos3  5900  tpostpos  5902  tpossym  5914  tposoprab  5918  frecsuclem3  6013  erth2  6174  qliftfun  6211  erovlem  6221  ecopovsym  6225  ecopovsymg  6228  th3qlem1  6231  dom2lem  6275  xpdom2  6328  ssfilem  6360  diffitest  6371  ac6sfi  6379  isoti  6420  cnvti  6432  ltexpi  6527  ordpipqqs  6564  ltexnqq  6598  enq0enq  6621  enq0sym  6622  enq0tr  6624  nqnq0pi  6628  genipv  6699  genprndl  6711  genprndu  6712  genpdisj  6713  genpassl  6714  genpassu  6715  addcomprg  6768  mulcomprg  6770  ltnqpr  6783  ltnqpri  6784  ltexprlemm  6790  ltexprlemdisj  6796  ltsrprg  6924  mulgt0sr  6954  elreal2  6999  ltresr  7007  ltresr2  7008  axprecex  7046  axpre-ltadd  7052  axpre-mulgt0  7053  axpre-mulext  7054  subcan2  7333  negcon1  7360  negcon2  7361  lt0neg1  7572  lt0neg2  7573  le0neg1  7574  le0neg2  7575  reapirr  7677  reapmul1  7695  reapneg  7697  remulext1  7699  apti  7722  negap0  7729  divmulap2  7764  reclt1  7974  recgt1  7975  suprleubex  8032  addltmul  8267  elznn0  8366  zapne  8422  zltlen  8426  nn0lt10b  8428  nn0lt2  8429  eluz1  8623  raluz  8666  rexuz  8668  qltlen  8725  cnref1o  8733  rpnegap  8766  ltxr  8849  xlt0neg1  8905  xlt0neg2  8906  xle0neg1  8907  xle0neg2  8908  elixx1  8920  elixx3g  8924  elioo2  8944  icc0r  8949  elicc4  8963  elioopnf  8990  elioomnf  8991  iooneg  9010  iccneg  9011  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  iccf1o  9026  elfz1  9034  0fz1  9064  fzpr  9094  fzdifsuc  9098  uzsplit  9109  elfzm1b  9115  elfzp12  9116  fznn0  9129  exfzdc  9249  flqeqceilz  9320  zmodid2  9354  expap0  9506  bernneq  9593  sqrtmsq2i  10021  maxclpr  10108  minmax  10112  clim0  10124  climrecvg1n  10185  dvdsval2  10198  odd2np1lem  10271  even2n  10273  divalgb  10325  divalgmod  10327  zsupcllemstep  10341  gcddvds  10355  bezoutlemmain  10387  isprm3  10500  prmind2  10502  dvdsprime  10504  coprm  10523  prmdvdsexp  10527  sqrt2irr  10541  sqpweven  10553  2sqpwodd  10554