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  874  pm5.75  947  xordidc  1378  19.17  1536  alexdc  1599  nf4dc  1649  abeq2d  2253  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvrab  2687  ceqsralt  2716  ralab2  2852  rexab2  2854  euxfr2dc  2873  reu7  2883  reu8  2884  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  ralss  3168  rexss  3169  prssg  3685  2ralunsn  3733  eluniab  3756  elintab  3790  dfiun2g  3853  dfiin2g  3854  cbvopab1  4009  cbvmpt  4031  axsep2  4055  bnd2  4105  opeqsn  4182  reusv3  4389  tfisi  4509  opeliunxp  4602  eliunxp  4686  relop  4697  eldm2g  4743  reldm0  4765  relrn0  4809  xpmlem  4967  elxp5  5035  cnvpom  5089  cbviota  5101  iota1  5110  sniota  5123  fncnv  5197  fnres  5247  brprcneu  5422  fnopfvb  5471  fvelrnb  5477  fvelimab  5485  fvopab3g  5502  eqfnfv3  5528  eqfnfv2f  5530  fvreseq  5532  fnreseql  5538  rexsupp  5552  respreima  5556  rexrn  5565  ralrn  5566  f1ompt  5579  fsn  5600  fconstfvm  5646  fconst3m  5647  fconst4m  5648  foima2  5661  rexima  5664  ralima  5665  dff13  5677  foeqcnvco  5699  fliftfun  5705  isocnv  5720  isoini  5727  f1oiso  5735  cbvriota  5748  eusvobj2  5768  oprabid  5811  eloprabga  5866  resoprab  5875  eqfnov  5885  eqfnov2  5886  ov6g  5916  funimassov  5928  ovelimab  5929  caovord2  5951  releldm2  6091  dfoprab4  6098  xporderlem  6136  poxp  6137  f1od2  6140  mpoxopovel  6146  brtpos2  6156  brtpos0  6157  rntpos  6162  dftpos3  6167  tpostpos  6169  tpossym  6181  tposoprab  6185  tfrcllemres  6267  frecabcl  6304  frecsuclem  6311  erth2  6482  qliftfun  6519  erovlem  6529  ecopovsym  6533  ecopovsymg  6536  th3qlem1  6539  mapdm0  6565  elpmg  6566  elpm2g  6567  map0e  6588  dom2lem  6674  mapsnen  6713  xpdom2  6733  xpf1o  6746  mapen  6748  ssfilem  6777  diffitest  6789  ac6sfi  6800  isoti  6902  cnvti  6914  omp1eomlem  6987  ismkvnex  7037  ltexpi  7169  ordpipqqs  7206  ltexnqq  7240  enq0enq  7263  enq0sym  7264  enq0tr  7266  nqnq0pi  7270  genipv  7341  genprndl  7353  genprndu  7354  genpdisj  7355  genpassl  7356  genpassu  7357  addcomprg  7410  mulcomprg  7412  ltnqpr  7425  ltnqpri  7426  ltexprlemm  7432  ltexprlemdisj  7438  suplocexprlemmu  7550  suplocexprlemdisj  7552  ltsrprg  7579  mulgt0sr  7610  elreal2  7662  ltresr  7671  ltresr2  7672  axprecex  7712  axpre-ltadd  7718  axpre-mulgt0  7719  axpre-mulext  7720  axpre-suploclemres  7733  subcan2  8011  negcon1  8038  negcon2  8039  lt0neg1  8254  lt0neg2  8255  le0neg1  8256  le0neg2  8257  reapirr  8363  reapmul1  8381  reapneg  8383  remulext1  8385  apti  8408  negap0  8416  divmulap2  8460  reclt1  8678  recgt1  8679  suprleubex  8736  addltmul  8980  elznn0  9093  zapne  9149  zltlen  9153  nn0lt10b  9155  nn0lt2  9156  eluz1  9354  raluz  9400  rexuz  9402  qltlen  9459  cnref1o  9469  rpnegap  9503  ltxr  9592  xlt0neg1  9651  xlt0neg2  9652  xle0neg1  9653  xle0neg2  9654  elixx1  9710  elixx3g  9714  elioo2  9734  icc0r  9739  elicc4  9753  elioopnf  9780  elioomnf  9781  iooneg  9801  iccneg  9802  iccshftr  9807  iccshftl  9809  iccdil  9811  icccntr  9813  iccf1o  9817  elfz1  9826  0fz1  9856  fzpr  9888  fzdifsuc  9892  uzsplit  9903  elfzm1b  9909  elfzp12  9910  fznn0  9924  exfzdc  10048  flqeqceilz  10122  zmodid2  10156  expap0  10354  bernneq  10443  hasheqf1o  10563  hashfacen  10611  sqrtmsq2i  10939  maxclpr  11026  minmax  11033  xrmaxlesup  11060  xrnegiso  11063  xrnegcon1d  11065  xrminmax  11066  clim0  11086  climrecvg1n  11149  summodc  11184  fsumsplit  11208  mertenslem2  11337  prodmodc  11379  dvdsval2  11532  odd2np1lem  11605  even2n  11607  divalgb  11658  divalgmod  11660  zsupcllemstep  11674  gcddvds  11688  bezoutlemmain  11722  isprm3  11835  prmind2  11837  dvdsprime  11839  coprm  11858  prmdvdsexp  11862  sqrt2irr  11876  sqpweven  11889  2sqpwodd  11890  elrest  12166  istopon  12219  isbasis2g  12251  isbasis3g  12252  tgss2  12287  bastop1  12291  iscld  12311  ntreq0  12340  restsn  12388  restopn2  12391  lmbr  12421  cnptoprest2  12448  txbas  12466  eltx  12467  txlm  12487  ishmeo  12512  hmeoimaf1o  12522  ispsmet  12531  ismet  12552  isxmet  12553  ismet2  12562  metn0  12586  elblps  12598  elbl  12599  bdbl  12711  qtopbasss  12729  elcncf  12768  ellimc3apf  12837  sincosq1sgn  12955  sincosq2sgn  12956  cos11  12982  logrpap0b  13005  subctctexmid  13369  iooref1o  13426