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  896  pm5.75  971  xordidc  1444  19.17  1605  alexdc  1668  nf4dc  1718  abeq2d  2347  eqabrd  2372  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvrab  2813  ceqsralt  2843  ralab2  2984  rexab2  2986  euxfr2dc  3005  reu7  3015  reu8  3016  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  ralss  3308  rexss  3309  elif  3638  prssg  3856  2ralunsn  3908  eluniab  3931  elintab  3965  dfiun2g  4028  dfiin2g  4029  cbvopab1  4188  cbvmpt  4210  axsep2  4234  bnd2  4291  opeqsn  4374  reusv3  4586  tfisi  4714  opeliunxp  4810  eliunxp  4899  relop  4910  eldm2g  4957  reldm0  4979  relrn0  5024  restidsing  5099  xpmlem  5188  elxp5  5256  cnvpom  5310  cbviota  5322  iota1  5332  sniota  5348  fncnv  5427  fnres  5480  brprcneu  5668  fnopfvb  5721  fvelrnb  5729  fvelimab  5738  fvopab3g  5755  eqfnfv3  5782  eqfnfv2f  5784  fvreseq  5786  fnreseql  5793  respreima  5810  rexrn  5819  ralrn  5820  f1ompt  5833  fsn  5854  fconstfvm  5907  fconst3m  5908  fconst4m  5909  foima2  5930  rexima  5933  ralima  5934  dff13  5947  foeqcnvco  5969  fliftfun  5975  isocnv  5990  isoini  5997  f1oiso  6005  cbvriota  6023  riotaeqimp  6036  eusvobj2  6044  oprabid  6090  eloprabga  6148  resoprab  6157  eqfnov  6168  eqfnov2  6169  ov6g  6200  funimassov  6212  ovelimab  6213  caovord2  6235  uchoice  6344  releldm2  6392  dfoprab4  6399  xporderlem  6440  poxp  6441  f1od2  6444  elsuppfng  6455  elsuppfn  6456  rexsupp  6466  mpoxopovel  6485  brtpos2  6495  brtpos0  6496  rntpos  6501  dftpos3  6506  tpostpos  6508  tpossym  6520  tposoprab  6524  tfrcllemres  6606  frecabcl  6643  frecsuclem  6650  erth2  6827  qliftfun  6864  erovlem  6874  ecopovsym  6878  ecopovsymg  6881  th3qlem1  6884  mapdm0  6910  elpmg  6911  elpm2g  6912  map0e  6933  dom2lem  7024  mapsnend  7065  mapsnen  7066  xpdom2  7095  xpf1o  7110  mapen  7112  ssfilem  7143  ssfilemd  7145  diffitest  7157  ac6sfi  7168  eqsndc  7176  ss1o0el1o  7186  2omap  7282  isoti  7311  cnvti  7323  omp1eomlem  7398  ismkvnex  7459  nninfwlporlemd  7476  en2prde  7503  netap  7584  2omotaplemap  7587  ltexpi  7668  ordpipqqs  7705  ltexnqq  7739  enq0enq  7762  enq0sym  7763  enq0tr  7765  nqnq0pi  7769  genipv  7840  genprndl  7852  genprndu  7853  genpdisj  7854  genpassl  7855  genpassu  7856  addcomprg  7909  mulcomprg  7911  ltnqpr  7924  ltnqpri  7925  ltexprlemm  7931  ltexprlemdisj  7937  suplocexprlemmu  8049  suplocexprlemdisj  8051  ltsrprg  8078  mulgt0sr  8109  elreal2  8161  ltresr  8170  ltresr2  8171  axprecex  8211  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  axpre-suploclemres  8232  subcan2  8514  negcon1  8541  negcon2  8542  lt0neg1  8759  lt0neg2  8760  le0neg1  8761  le0neg2  8762  reapirr  8868  reapmul1  8886  reapneg  8888  remulext1  8890  apti  8913  negap0  8921  divmulap2  8967  reclt1  9187  recgt1  9188  suprleubex  9245  addltmul  9492  elznn0  9609  zapne  9669  zltlen  9674  nn0lt10b  9676  nn0lt2  9677  eluz1  9875  raluz  9928  rexuz  9930  qltlen  9990  cnref1o  10001  rpnegap  10037  ltxr  10127  xlt0neg1  10190  xlt0neg2  10191  xle0neg1  10192  xle0neg2  10193  elixx1  10249  elixx3g  10253  elioo2  10273  icc0r  10278  elicc4  10292  elioopnf  10319  elioomnf  10320  iooneg  10340  iccneg  10341  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  iccf1o  10357  elfz1  10366  0fz1  10399  fzpr  10433  fzdifsuc  10437  uzsplit  10448  elfzm1b  10454  elfzp12  10455  fznn0  10469  exfzdc  10608  zsupcllemstep  10611  flqeqceilz  10704  zmodid2  10738  expap0  10955  qsqeqor  11036  bernneq  11047  hasheqf1o  11173  ssenneg  11229  hashfibclem  11231  hashfacen  11233  ccatrn  11322  pfxsuffeqwrdeq  11415  wrd2ind  11440  sqrtmsq2i  11845  maxclpr  11932  minmax  11940  xrmaxlesup  11969  xrnegiso  11972  xrnegcon1d  11974  xrminmax  11975  clim0  11995  climrecvg1n  12058  summodc  12094  fsumsplit  12118  mertenslem2  12247  prodmodc  12289  fprodsplitdc  12307  fprod2dlemstep  12333  dvdsval2  12501  odd2np1lem  12583  even2n  12585  divalgb  12636  divalgmod  12638  bitsval  12654  bitsmod  12667  gcddvds  12684  bezoutlemmain  12719  nnwofdc  12759  isprm3  12840  prmind2  12842  dvdsprime  12844  coprm  12866  prmdvdsexp  12870  sqrt2irr  12884  sqpweven  12897  2sqpwodd  12898  pythagtriplem2  12989  pythagtrip  13006  pceu  13018  pc11  13054  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  elrest  13543  grpsubeq0  13841  grpsubadd  13843  issubg3  13945  isnsg  13955  eqger  13977  eqglact  13978  eqgid  13979  srgfcl  14216  dvdsrtr  14346  dvdsr02  14350  isunitd  14351  isrhm  14403  isrim0  14406  subsubrng2  14461  subsubrg2  14492  issubrg3  14493  opprdomnbg  14521  2idlelb  14779  mplelbascoe  14973  istopon  15004  isbasis2g  15036  isbasis3g  15037  tgss2  15070  bastop1  15074  iscld  15094  ntreq0  15123  restsn  15171  restopn2  15174  lmbr  15204  cnptoprest2  15231  txbas  15249  eltx  15250  txlm  15270  ishmeo  15295  hmeoimaf1o  15305  ispsmet  15314  ismet  15335  isxmet  15336  ismet2  15345  metn0  15369  elblps  15381  elbl  15382  bdbl  15494  qtopbasss  15512  elcncf  15564  ellimc3apf  15651  elply  15725  sincosq1sgn  15817  sincosq2sgn  15818  cos11  15844  logrpap0b  15867  lgsdir2lem4  16030  gausslemma2dlem0i  16056  lgsquadlem2  16077  m1lgs  16084  2lgsoddprmlem3  16110  2sqlem6  16119  2sqlem9  16123  2sqlem10  16124  vtxdfifiun  16418  wlkl1loop  16479  wlkv0  16490  wlklenvclwlk  16494  upgr2wlkdc  16498  isclwwlk  16515  isclwwlkng  16527  isclwwlknx  16537  clwwlkn2  16542  eupth2lem2dc  16580  eupth2lem3lem6fi  16592  pw1map  16895  subctctexmid  16900  iooref1o  16944  iswomni0  16962