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  895  pm5.75  970  xordidc  1443  19.17  1604  alexdc  1667  nf4dc  1718  abeq2d  2344  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvrab  2800  ceqsralt  2830  ralab2  2970  rexab2  2972  euxfr2dc  2991  reu7  3001  reu8  3002  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  ralss  3293  rexss  3294  elif  3617  prssg  3830  2ralunsn  3882  eluniab  3905  elintab  3939  dfiun2g  4002  dfiin2g  4003  cbvopab1  4162  cbvmpt  4184  axsep2  4208  bnd2  4263  opeqsn  4345  reusv3  4557  tfisi  4685  opeliunxp  4781  eliunxp  4869  relop  4880  eldm2g  4927  reldm0  4949  relrn0  4994  restidsing  5069  xpmlem  5157  elxp5  5225  cnvpom  5279  cbviota  5291  iota1  5301  sniota  5317  fncnv  5396  fnres  5449  brprcneu  5632  fnopfvb  5685  fvelrnb  5693  fvelimab  5702  fvopab3g  5719  eqfnfv3  5746  eqfnfv2f  5748  fvreseq  5750  fnreseql  5757  rexsupp  5771  respreima  5775  rexrn  5784  ralrn  5785  f1ompt  5798  fsn  5819  fconstfvm  5871  fconst3m  5872  fconst4m  5873  foima2  5891  rexima  5894  ralima  5895  dff13  5908  foeqcnvco  5930  fliftfun  5936  isocnv  5951  isoini  5958  f1oiso  5966  cbvriota  5982  riotaeqimp  5995  eusvobj2  6003  oprabid  6049  eloprabga  6107  resoprab  6116  eqfnov  6127  eqfnov2  6128  ov6g  6159  funimassov  6171  ovelimab  6172  caovord2  6194  uchoice  6299  releldm2  6347  dfoprab4  6354  xporderlem  6395  poxp  6396  f1od2  6399  mpoxopovel  6406  brtpos2  6416  brtpos0  6417  rntpos  6422  dftpos3  6427  tpostpos  6429  tpossym  6441  tposoprab  6445  tfrcllemres  6527  frecabcl  6564  frecsuclem  6571  erth2  6748  qliftfun  6785  erovlem  6795  ecopovsym  6799  ecopovsymg  6802  th3qlem1  6805  mapdm0  6831  elpmg  6832  elpm2g  6833  map0e  6854  dom2lem  6944  mapsnen  6985  xpdom2  7014  xpf1o  7029  mapen  7031  ssfilem  7061  ssfilemd  7063  diffitest  7075  ac6sfi  7086  eqsndc  7094  ss1o0el1o  7104  isoti  7205  cnvti  7217  omp1eomlem  7292  ismkvnex  7353  nninfwlporlemd  7370  en2prde  7397  netap  7472  2omotaplemap  7475  ltexpi  7556  ordpipqqs  7593  ltexnqq  7627  enq0enq  7650  enq0sym  7651  enq0tr  7653  nqnq0pi  7657  genipv  7728  genprndl  7740  genprndu  7741  genpdisj  7742  genpassl  7743  genpassu  7744  addcomprg  7797  mulcomprg  7799  ltnqpr  7812  ltnqpri  7813  ltexprlemm  7819  ltexprlemdisj  7825  suplocexprlemmu  7937  suplocexprlemdisj  7939  ltsrprg  7966  mulgt0sr  7997  elreal2  8049  ltresr  8058  ltresr2  8059  axprecex  8099  axpre-ltadd  8105  axpre-mulgt0  8106  axpre-mulext  8107  axpre-suploclemres  8120  subcan2  8403  negcon1  8430  negcon2  8431  lt0neg1  8647  lt0neg2  8648  le0neg1  8649  le0neg2  8650  reapirr  8756  reapmul1  8774  reapneg  8776  remulext1  8778  apti  8801  negap0  8809  divmulap2  8855  reclt1  9075  recgt1  9076  suprleubex  9133  addltmul  9380  elznn0  9493  zapne  9553  zltlen  9557  nn0lt10b  9559  nn0lt2  9560  eluz1  9758  raluz  9811  rexuz  9813  qltlen  9873  cnref1o  9884  rpnegap  9920  ltxr  10009  xlt0neg1  10072  xlt0neg2  10073  xle0neg1  10074  xle0neg2  10075  elixx1  10131  elixx3g  10135  elioo2  10155  icc0r  10160  elicc4  10174  elioopnf  10201  elioomnf  10202  iooneg  10222  iccneg  10223  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  iccf1o  10238  elfz1  10247  0fz1  10279  fzpr  10311  fzdifsuc  10315  uzsplit  10326  elfzm1b  10332  elfzp12  10333  fznn0  10347  exfzdc  10485  zsupcllemstep  10488  flqeqceilz  10579  zmodid2  10613  expap0  10830  qsqeqor  10911  bernneq  10921  hasheqf1o  11046  hashfacen  11099  ccatrn  11185  pfxsuffeqwrdeq  11278  wrd2ind  11303  sqrtmsq2i  11695  maxclpr  11782  minmax  11790  xrmaxlesup  11819  xrnegiso  11822  xrnegcon1d  11824  xrminmax  11825  clim0  11845  climrecvg1n  11908  summodc  11943  fsumsplit  11967  mertenslem2  12096  prodmodc  12138  fprodsplitdc  12156  fprod2dlemstep  12182  dvdsval2  12350  odd2np1lem  12432  even2n  12434  divalgb  12485  divalgmod  12487  bitsval  12503  bitsmod  12516  gcddvds  12533  bezoutlemmain  12568  nnwofdc  12608  isprm3  12689  prmind2  12691  dvdsprime  12693  coprm  12715  prmdvdsexp  12719  sqrt2irr  12733  sqpweven  12746  2sqpwodd  12747  pythagtriplem2  12838  pythagtrip  12855  pceu  12867  pc11  12903  elrest  13328  grpsubeq0  13668  grpsubadd  13670  issubg3  13778  isnsg  13788  eqger  13810  eqglact  13811  eqgid  13812  srgfcl  13985  dvdsrtr  14114  dvdsr02  14118  isunitd  14119  isrhm  14171  isrim0  14174  subsubrng2  14228  subsubrg2  14259  issubrg3  14260  opprdomnbg  14287  2idlelb  14518  mplelbascoe  14705  istopon  14736  isbasis2g  14768  isbasis3g  14769  tgss2  14802  bastop1  14806  iscld  14826  ntreq0  14855  restsn  14903  restopn2  14906  lmbr  14936  cnptoprest2  14963  txbas  14981  eltx  14982  txlm  15002  ishmeo  15027  hmeoimaf1o  15037  ispsmet  15046  ismet  15067  isxmet  15068  ismet2  15077  metn0  15101  elblps  15113  elbl  15114  bdbl  15226  qtopbasss  15244  elcncf  15296  ellimc3apf  15383  elply  15457  sincosq1sgn  15549  sincosq2sgn  15550  cos11  15576  logrpap0b  15599  lgsdir2lem4  15759  gausslemma2dlem0i  15785  lgsquadlem2  15806  m1lgs  15813  2lgsoddprmlem3  15839  2sqlem6  15848  2sqlem9  15852  2sqlem10  15853  vtxdfifiun  16147  wlkl1loop  16208  wlkv0  16219  wlklenvclwlk  16223  upgr2wlkdc  16227  isclwwlk  16244  isclwwlkng  16256  isclwwlknx  16266  clwwlkn2  16271  eupth2lem2dc  16309  2omap  16594  pw1map  16596  subctctexmid  16601  iooref1o  16638  iswomni0  16655