Theorem bitrdi 196

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

Hypotheses

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

Assertion

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

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		bitrdi.2	. . 3 |- ( ch <-> th )
3	2	a1i 9	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 188	1 |- ( ph -> ( ps <-> th ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2di  197  bitr4di  198  3bitr3g  222  bibi2i  227  ibibr  246  biancomd  271  imanst  888  pm5.75  962  xordidc  1399  19.17  1556  alexdc  1619  nf4dc  1670  abeq2d  2290  cbvralf  2696  cbvrexf  2697  cbvreu  2701  cbvrab  2735  ceqsralt  2764  ralab2  2901  rexab2  2903  euxfr2dc  2922  reu7  2932  reu8  2933  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  ralss  3221  rexss  3222  prssg  3749  2ralunsn  3798  eluniab  3821  elintab  3855  dfiun2g  3918  dfiin2g  3919  cbvopab1  4076  cbvmpt  4098  axsep2  4122  bnd2  4173  opeqsn  4252  reusv3  4460  tfisi  4586  opeliunxp  4681  eliunxp  4766  relop  4777  eldm2g  4823  reldm0  4845  relrn0  4889  restidsing  4963  xpmlem  5049  elxp5  5117  cnvpom  5171  cbviota  5183  iota1  5192  sniota  5207  fncnv  5282  fnres  5332  brprcneu  5508  fnopfvb  5557  fvelrnb  5563  fvelimab  5572  fvopab3g  5589  eqfnfv3  5615  eqfnfv2f  5617  fvreseq  5619  fnreseql  5626  rexsupp  5640  respreima  5644  rexrn  5653  ralrn  5654  f1ompt  5667  fsn  5688  fconstfvm  5734  fconst3m  5735  fconst4m  5736  foima2  5752  rexima  5755  ralima  5756  dff13  5768  foeqcnvco  5790  fliftfun  5796  isocnv  5811  isoini  5818  f1oiso  5826  cbvriota  5840  eusvobj2  5860  oprabid  5906  eloprabga  5961  resoprab  5970  eqfnov  5980  eqfnov2  5981  ov6g  6011  funimassov  6023  ovelimab  6024  caovord2  6046  releldm2  6185  dfoprab4  6192  xporderlem  6231  poxp  6232  f1od2  6235  mpoxopovel  6241  brtpos2  6251  brtpos0  6252  rntpos  6257  dftpos3  6262  tpostpos  6264  tpossym  6276  tposoprab  6280  tfrcllemres  6362  frecabcl  6399  frecsuclem  6406  erth2  6579  qliftfun  6616  erovlem  6626  ecopovsym  6630  ecopovsymg  6633  th3qlem1  6636  mapdm0  6662  elpmg  6663  elpm2g  6664  map0e  6685  dom2lem  6771  mapsnen  6810  xpdom2  6830  xpf1o  6843  mapen  6845  ssfilem  6874  diffitest  6886  ac6sfi  6897  ss1o0el1o  6911  isoti  7005  cnvti  7017  omp1eomlem  7092  ismkvnex  7152  nninfwlporlemd  7169  netap  7252  2omotaplemap  7255  ltexpi  7335  ordpipqqs  7372  ltexnqq  7406  enq0enq  7429  enq0sym  7430  enq0tr  7432  nqnq0pi  7436  genipv  7507  genprndl  7519  genprndu  7520  genpdisj  7521  genpassl  7522  genpassu  7523  addcomprg  7576  mulcomprg  7578  ltnqpr  7591  ltnqpri  7592  ltexprlemm  7598  ltexprlemdisj  7604  suplocexprlemmu  7716  suplocexprlemdisj  7718  ltsrprg  7745  mulgt0sr  7776  elreal2  7828  ltresr  7837  ltresr2  7838  axprecex  7878  axpre-ltadd  7884  axpre-mulgt0  7885  axpre-mulext  7886  axpre-suploclemres  7899  subcan2  8180  negcon1  8207  negcon2  8208  lt0neg1  8423  lt0neg2  8424  le0neg1  8425  le0neg2  8426  reapirr  8532  reapmul1  8550  reapneg  8552  remulext1  8554  apti  8577  negap0  8585  divmulap2  8631  reclt1  8851  recgt1  8852  suprleubex  8909  addltmul  9153  elznn0  9266  zapne  9325  zltlen  9329  nn0lt10b  9331  nn0lt2  9332  eluz1  9530  raluz  9576  rexuz  9578  qltlen  9638  cnref1o  9648  rpnegap  9684  ltxr  9773  xlt0neg1  9836  xlt0neg2  9837  xle0neg1  9838  xle0neg2  9839  elixx1  9895  elixx3g  9899  elioo2  9919  icc0r  9924  elicc4  9938  elioopnf  9965  elioomnf  9966  iooneg  9986  iccneg  9987  iccshftr  9992  iccshftl  9994  iccdil  9996  icccntr  9998  iccf1o  10002  elfz1  10011  0fz1  10042  fzpr  10074  fzdifsuc  10078  uzsplit  10089  elfzm1b  10095  elfzp12  10096  fznn0  10110  exfzdc  10237  flqeqceilz  10315  zmodid2  10349  expap0  10547  qsqeqor  10627  bernneq  10637  hasheqf1o  10760  hashfacen  10811  sqrtmsq2i  11139  maxclpr  11226  minmax  11233  xrmaxlesup  11262  xrnegiso  11265  xrnegcon1d  11267  xrminmax  11268  clim0  11288  climrecvg1n  11351  summodc  11386  fsumsplit  11410  mertenslem2  11539  prodmodc  11581  fprodsplitdc  11599  fprod2dlemstep  11625  dvdsval2  11792  odd2np1lem  11871  even2n  11873  divalgb  11924  divalgmod  11926  zsupcllemstep  11940  gcddvds  11958  bezoutlemmain  11993  nnwofdc  12033  isprm3  12112  prmind2  12114  dvdsprime  12116  coprm  12138  prmdvdsexp  12142  sqrt2irr  12156  sqpweven  12169  2sqpwodd  12170  pythagtriplem2  12260  pythagtrip  12277  pceu  12289  pc11  12324  elrest  12689  grpsubeq0  12950  grpsubadd  12952  issubg3  13045  isnsg  13055  eqger  13076  eqglact  13077  eqgid  13078  srgfcl  13149  dvdsrtr  13263  dvdsr02  13267  isunitd  13268  subsubrg2  13367  issubrg3  13368  istopon  13444  isbasis2g  13476  isbasis3g  13477  tgss2  13510  bastop1  13514  iscld  13534  ntreq0  13563  restsn  13611  restopn2  13614  lmbr  13644  cnptoprest2  13671  txbas  13689  eltx  13690  txlm  13710  ishmeo  13735  hmeoimaf1o  13745  ispsmet  13754  ismet  13775  isxmet  13776  ismet2  13785  metn0  13809  elblps  13821  elbl  13822  bdbl  13934  qtopbasss  13952  elcncf  13991  ellimc3apf  14060  sincosq1sgn  14178  sincosq2sgn  14179  cos11  14205  logrpap0b  14228  lgsdir2lem4  14363  2sqlem6  14387  2sqlem9  14391  2sqlem10  14392  subctctexmid  14670  iooref1o  14702  iswomni0  14719