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  2345  eqabrd  2370  cbvralf  2769  cbvrexf  2770  cbvreu  2776  cbvrab  2811  ceqsralt  2841  ralab2  2981  rexab2  2983  euxfr2dc  3002  reu7  3012  reu8  3013  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  ralss  3304  rexss  3305  elif  3634  prssg  3851  2ralunsn  3903  eluniab  3926  elintab  3960  dfiun2g  4023  dfiin2g  4024  cbvopab1  4183  cbvmpt  4205  axsep2  4229  bnd2  4286  opeqsn  4369  reusv3  4581  tfisi  4709  opeliunxp  4805  eliunxp  4894  relop  4905  eldm2g  4952  reldm0  4974  relrn0  5019  restidsing  5094  xpmlem  5183  elxp5  5251  cnvpom  5305  cbviota  5317  iota1  5327  sniota  5343  fncnv  5422  fnres  5475  brprcneu  5663  fnopfvb  5716  fvelrnb  5724  fvelimab  5733  fvopab3g  5750  eqfnfv3  5777  eqfnfv2f  5779  fvreseq  5781  fnreseql  5788  respreima  5805  rexrn  5814  ralrn  5815  f1ompt  5828  fsn  5849  fconstfvm  5902  fconst3m  5903  fconst4m  5904  foima2  5924  rexima  5927  ralima  5928  dff13  5941  foeqcnvco  5963  fliftfun  5969  isocnv  5984  isoini  5991  f1oiso  5999  cbvriota  6015  riotaeqimp  6028  eusvobj2  6036  oprabid  6082  eloprabga  6140  resoprab  6149  eqfnov  6160  eqfnov2  6161  ov6g  6192  funimassov  6204  ovelimab  6205  caovord2  6227  uchoice  6331  releldm2  6379  dfoprab4  6386  xporderlem  6427  poxp  6428  f1od2  6431  elsuppfng  6442  elsuppfn  6443  rexsupp  6453  mpoxopovel  6472  brtpos2  6482  brtpos0  6483  rntpos  6488  dftpos3  6493  tpostpos  6495  tpossym  6507  tposoprab  6511  tfrcllemres  6593  frecabcl  6630  frecsuclem  6637  erth2  6814  qliftfun  6851  erovlem  6861  ecopovsym  6865  ecopovsymg  6868  th3qlem1  6871  mapdm0  6897  elpmg  6898  elpm2g  6899  map0e  6920  dom2lem  7011  mapsnend  7052  mapsnen  7053  xpdom2  7082  xpf1o  7097  mapen  7099  ssfilem  7130  ssfilemd  7132  diffitest  7144  ac6sfi  7155  eqsndc  7163  ss1o0el1o  7173  2omap  7269  isoti  7298  cnvti  7310  omp1eomlem  7385  ismkvnex  7446  nninfwlporlemd  7463  en2prde  7490  netap  7568  2omotaplemap  7571  ltexpi  7652  ordpipqqs  7689  ltexnqq  7723  enq0enq  7746  enq0sym  7747  enq0tr  7749  nqnq0pi  7753  genipv  7824  genprndl  7836  genprndu  7837  genpdisj  7838  genpassl  7839  genpassu  7840  addcomprg  7893  mulcomprg  7895  ltnqpr  7908  ltnqpri  7909  ltexprlemm  7915  ltexprlemdisj  7921  suplocexprlemmu  8033  suplocexprlemdisj  8035  ltsrprg  8062  mulgt0sr  8093  elreal2  8145  ltresr  8154  ltresr2  8155  axprecex  8195  axpre-ltadd  8201  axpre-mulgt0  8202  axpre-mulext  8203  axpre-suploclemres  8216  subcan2  8498  negcon1  8525  negcon2  8526  lt0neg1  8742  lt0neg2  8743  le0neg1  8744  le0neg2  8745  reapirr  8851  reapmul1  8869  reapneg  8871  remulext1  8873  apti  8896  negap0  8904  divmulap2  8950  reclt1  9170  recgt1  9171  suprleubex  9228  addltmul  9475  elznn0  9592  zapne  9652  zltlen  9656  nn0lt10b  9658  nn0lt2  9659  eluz1  9857  raluz  9910  rexuz  9912  qltlen  9972  cnref1o  9983  rpnegap  10019  ltxr  10108  xlt0neg1  10171  xlt0neg2  10172  xle0neg1  10173  xle0neg2  10174  elixx1  10230  elixx3g  10234  elioo2  10254  icc0r  10259  elicc4  10273  elioopnf  10300  elioomnf  10301  iooneg  10321  iccneg  10322  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  iccf1o  10338  elfz1  10347  0fz1  10379  fzpr  10411  fzdifsuc  10415  uzsplit  10426  elfzm1b  10432  elfzp12  10433  fznn0  10447  exfzdc  10586  zsupcllemstep  10589  flqeqceilz  10680  zmodid2  10714  expap0  10931  qsqeqor  11012  bernneq  11022  hasheqf1o  11148  ssenneg  11204  hashfibclem  11206  hashfacen  11208  ccatrn  11297  pfxsuffeqwrdeq  11390  wrd2ind  11415  sqrtmsq2i  11820  maxclpr  11907  minmax  11915  xrmaxlesup  11944  xrnegiso  11947  xrnegcon1d  11949  xrminmax  11950  clim0  11970  climrecvg1n  12033  summodc  12069  fsumsplit  12093  mertenslem2  12222  prodmodc  12264  fprodsplitdc  12282  fprod2dlemstep  12308  dvdsval2  12476  odd2np1lem  12558  even2n  12560  divalgb  12611  divalgmod  12613  bitsval  12629  bitsmod  12642  gcddvds  12659  bezoutlemmain  12694  nnwofdc  12734  isprm3  12815  prmind2  12817  dvdsprime  12819  coprm  12841  prmdvdsexp  12845  sqrt2irr  12859  sqpweven  12872  2sqpwodd  12873  pythagtriplem2  12964  pythagtrip  12981  pceu  12993  pc11  13029  elrest  13459  grpsubeq0  13799  grpsubadd  13801  issubg3  13909  isnsg  13919  eqger  13941  eqglact  13942  eqgid  13943  srgfcl  14117  dvdsrtr  14246  dvdsr02  14250  isunitd  14251  isrhm  14303  isrim0  14306  subsubrng2  14360  subsubrg2  14391  issubrg3  14392  opprdomnbg  14420  2idlelb  14653  mplelbascoe  14847  istopon  14878  isbasis2g  14910  isbasis3g  14911  tgss2  14944  bastop1  14948  iscld  14968  ntreq0  14997  restsn  15045  restopn2  15048  lmbr  15078  cnptoprest2  15105  txbas  15123  eltx  15124  txlm  15144  ishmeo  15169  hmeoimaf1o  15179  ispsmet  15188  ismet  15209  isxmet  15210  ismet2  15219  metn0  15243  elblps  15255  elbl  15256  bdbl  15368  qtopbasss  15386  elcncf  15438  ellimc3apf  15525  elply  15599  sincosq1sgn  15691  sincosq2sgn  15692  cos11  15718  logrpap0b  15741  lgsdir2lem4  15904  gausslemma2dlem0i  15930  lgsquadlem2  15951  m1lgs  15958  2lgsoddprmlem3  15984  2sqlem6  15993  2sqlem9  15997  2sqlem10  15998  vtxdfifiun  16292  wlkl1loop  16353  wlkv0  16364  wlklenvclwlk  16368  upgr2wlkdc  16372  isclwwlk  16389  isclwwlkng  16401  isclwwlknx  16411  clwwlkn2  16416  eupth2lem2dc  16454  eupth2lem3lem6fi  16466  pw1map  16769  subctctexmid  16774  iooref1o  16818  iswomni0  16836