Theorem syl6bb 195

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 187	1 |- ( ph -> ( ps <-> th ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl6rbb  196  syl6bbr  197  3bitr3g  221  bibi2i  226  ibibr  245  biancomd  269  imanst  873  pm5.75  946  xordidc  1377  19.17  1535  alexdc  1598  nf4dc  1648  abeq2d  2250  cbvralf  2646  cbvrexf  2647  cbvreu  2650  cbvrab  2679  ceqsralt  2708  ralab2  2843  rexab2  2845  euxfr2dc  2864  reu7  2874  reu8  2875  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  ralss  3158  rexss  3159  prssg  3672  2ralunsn  3720  eluniab  3743  elintab  3777  dfiun2g  3840  dfiin2g  3841  cbvopab1  3996  cbvmpt  4018  axsep2  4042  bnd2  4092  opeqsn  4169  reusv3  4376  tfisi  4496  opeliunxp  4589  eliunxp  4673  relop  4684  eldm2g  4730  reldm0  4752  relrn0  4796  xpmlem  4954  elxp5  5022  cnvpom  5076  cbviota  5088  iota1  5097  sniota  5110  fncnv  5184  fnres  5234  brprcneu  5407  fnopfvb  5456  fvelrnb  5462  fvelimab  5470  fvopab3g  5487  eqfnfv3  5513  eqfnfv2f  5515  fvreseq  5517  fnreseql  5523  rexsupp  5537  respreima  5541  rexrn  5550  ralrn  5551  f1ompt  5564  fsn  5585  fconstfvm  5631  fconst3m  5632  fconst4m  5633  foima2  5646  rexima  5649  ralima  5650  dff13  5662  foeqcnvco  5684  fliftfun  5690  isocnv  5705  isoini  5712  f1oiso  5720  cbvriota  5733  eusvobj2  5753  oprabid  5796  eloprabga  5851  resoprab  5860  eqfnov  5870  eqfnov2  5871  ov6g  5901  funimassov  5913  ovelimab  5914  caovord2  5936  releldm2  6076  dfoprab4  6083  xporderlem  6121  poxp  6122  f1od2  6125  mpoxopovel  6131  brtpos2  6141  brtpos0  6142  rntpos  6147  dftpos3  6152  tpostpos  6154  tpossym  6166  tposoprab  6170  tfrcllemres  6252  frecabcl  6289  frecsuclem  6296  erth2  6467  qliftfun  6504  erovlem  6514  ecopovsym  6518  ecopovsymg  6521  th3qlem1  6524  mapdm0  6550  elpmg  6551  elpm2g  6552  map0e  6573  dom2lem  6659  mapsnen  6698  xpdom2  6718  xpf1o  6731  mapen  6733  ssfilem  6762  diffitest  6774  ac6sfi  6785  isoti  6887  cnvti  6899  omp1eomlem  6972  ismkvnex  7022  ltexpi  7138  ordpipqqs  7175  ltexnqq  7209  enq0enq  7232  enq0sym  7233  enq0tr  7235  nqnq0pi  7239  genipv  7310  genprndl  7322  genprndu  7323  genpdisj  7324  genpassl  7325  genpassu  7326  addcomprg  7379  mulcomprg  7381  ltnqpr  7394  ltnqpri  7395  ltexprlemm  7401  ltexprlemdisj  7407  suplocexprlemmu  7519  suplocexprlemdisj  7521  ltsrprg  7548  mulgt0sr  7579  elreal2  7631  ltresr  7640  ltresr2  7641  axprecex  7681  axpre-ltadd  7687  axpre-mulgt0  7688  axpre-mulext  7689  axpre-suploclemres  7702  subcan2  7980  negcon1  8007  negcon2  8008  lt0neg1  8223  lt0neg2  8224  le0neg1  8225  le0neg2  8226  reapirr  8332  reapmul1  8350  reapneg  8352  remulext1  8354  apti  8377  negap0  8385  divmulap2  8429  reclt1  8647  recgt1  8648  suprleubex  8705  addltmul  8949  elznn0  9062  zapne  9118  zltlen  9122  nn0lt10b  9124  nn0lt2  9125  eluz1  9323  raluz  9366  rexuz  9368  qltlen  9425  cnref1o  9433  rpnegap  9467  ltxr  9555  xlt0neg1  9614  xlt0neg2  9615  xle0neg1  9616  xle0neg2  9617  elixx1  9673  elixx3g  9677  elioo2  9697  icc0r  9702  elicc4  9716  elioopnf  9743  elioomnf  9744  iooneg  9764  iccneg  9765  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  iccf1o  9780  elfz1  9788  0fz1  9818  fzpr  9850  fzdifsuc  9854  uzsplit  9865  elfzm1b  9871  elfzp12  9872  fznn0  9886  exfzdc  10010  flqeqceilz  10084  zmodid2  10118  expap0  10316  bernneq  10405  hasheqf1o  10524  hashfacen  10572  sqrtmsq2i  10900  maxclpr  10987  minmax  10994  xrmaxlesup  11021  xrnegiso  11024  xrnegcon1d  11026  xrminmax  11027  clim0  11047  climrecvg1n  11110  summodc  11145  fsumsplit  11169  mertenslem2  11298  dvdsval2  11485  odd2np1lem  11558  even2n  11560  divalgb  11611  divalgmod  11613  zsupcllemstep  11627  gcddvds  11641  bezoutlemmain  11675  isprm3  11788  prmind2  11790  dvdsprime  11792  coprm  11811  prmdvdsexp  11815  sqrt2irr  11829  sqpweven  11842  2sqpwodd  11843  elrest  12116  istopon  12169  isbasis2g  12201  isbasis3g  12202  tgss2  12237  bastop1  12241  iscld  12261  ntreq0  12290  restsn  12338  restopn2  12341  lmbr  12371  cnptoprest2  12398  txbas  12416  eltx  12417  txlm  12437  ishmeo  12462  hmeoimaf1o  12472  ispsmet  12481  ismet  12502  isxmet  12503  ismet2  12512  metn0  12536  elblps  12548  elbl  12549  bdbl  12661  qtopbasss  12679  elcncf  12718  ellimc3apf  12787  sincosq1sgn  12896  sincosq2sgn  12897  subctctexmid  13185