Theorem bitrdi 195

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 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:  bitr2di  196  bitr4di  197  3bitr3g  221  bibi2i  226  ibibr  245  biancomd  269  imanst  878  pm5.75  952  xordidc  1389  19.17  1544  alexdc  1607  nf4dc  1658  abeq2d  2278  cbvralf  2684  cbvrexf  2685  cbvreu  2689  cbvrab  2723  ceqsralt  2752  ralab2  2889  rexab2  2891  euxfr2dc  2910  reu7  2920  reu8  2921  cbvralcsf  3106  cbvrexcsf  3107  cbvreucsf  3108  cbvrabcsf  3109  ralss  3207  rexss  3208  prssg  3729  2ralunsn  3777  eluniab  3800  elintab  3834  dfiun2g  3897  dfiin2g  3898  cbvopab1  4054  cbvmpt  4076  axsep2  4100  bnd2  4151  opeqsn  4229  reusv3  4437  tfisi  4563  opeliunxp  4658  eliunxp  4742  relop  4753  eldm2g  4799  reldm0  4821  relrn0  4865  xpmlem  5023  elxp5  5091  cnvpom  5145  cbviota  5157  iota1  5166  sniota  5179  fncnv  5253  fnres  5303  brprcneu  5478  fnopfvb  5527  fvelrnb  5533  fvelimab  5541  fvopab3g  5558  eqfnfv3  5584  eqfnfv2f  5586  fvreseq  5588  fnreseql  5594  rexsupp  5608  respreima  5612  rexrn  5621  ralrn  5622  f1ompt  5635  fsn  5656  fconstfvm  5702  fconst3m  5703  fconst4m  5704  foima2  5719  rexima  5722  ralima  5723  dff13  5735  foeqcnvco  5757  fliftfun  5763  isocnv  5778  isoini  5785  f1oiso  5793  cbvriota  5807  eusvobj2  5827  oprabid  5870  eloprabga  5925  resoprab  5934  eqfnov  5944  eqfnov2  5945  ov6g  5975  funimassov  5987  ovelimab  5988  caovord2  6010  releldm2  6150  dfoprab4  6157  xporderlem  6195  poxp  6196  f1od2  6199  mpoxopovel  6205  brtpos2  6215  brtpos0  6216  rntpos  6221  dftpos3  6226  tpostpos  6228  tpossym  6240  tposoprab  6244  tfrcllemres  6326  frecabcl  6363  frecsuclem  6370  erth2  6542  qliftfun  6579  erovlem  6589  ecopovsym  6593  ecopovsymg  6596  th3qlem1  6599  mapdm0  6625  elpmg  6626  elpm2g  6627  map0e  6648  dom2lem  6734  mapsnen  6773  xpdom2  6793  xpf1o  6806  mapen  6808  ssfilem  6837  diffitest  6849  ac6sfi  6860  ss1o0el1o  6874  isoti  6968  cnvti  6980  omp1eomlem  7055  ismkvnex  7115  ltexpi  7274  ordpipqqs  7311  ltexnqq  7345  enq0enq  7368  enq0sym  7369  enq0tr  7371  nqnq0pi  7375  genipv  7446  genprndl  7458  genprndu  7459  genpdisj  7460  genpassl  7461  genpassu  7462  addcomprg  7515  mulcomprg  7517  ltnqpr  7530  ltnqpri  7531  ltexprlemm  7537  ltexprlemdisj  7543  suplocexprlemmu  7655  suplocexprlemdisj  7657  ltsrprg  7684  mulgt0sr  7715  elreal2  7767  ltresr  7776  ltresr2  7777  axprecex  7817  axpre-ltadd  7823  axpre-mulgt0  7824  axpre-mulext  7825  axpre-suploclemres  7838  subcan2  8119  negcon1  8146  negcon2  8147  lt0neg1  8362  lt0neg2  8363  le0neg1  8364  le0neg2  8365  reapirr  8471  reapmul1  8489  reapneg  8491  remulext1  8493  apti  8516  negap0  8524  divmulap2  8568  reclt1  8787  recgt1  8788  suprleubex  8845  addltmul  9089  elznn0  9202  zapne  9261  zltlen  9265  nn0lt10b  9267  nn0lt2  9268  eluz1  9466  raluz  9512  rexuz  9514  qltlen  9574  cnref1o  9584  rpnegap  9618  ltxr  9707  xlt0neg1  9770  xlt0neg2  9771  xle0neg1  9772  xle0neg2  9773  elixx1  9829  elixx3g  9833  elioo2  9853  icc0r  9858  elicc4  9872  elioopnf  9899  elioomnf  9900  iooneg  9920  iccneg  9921  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  iccf1o  9936  elfz1  9945  0fz1  9976  fzpr  10008  fzdifsuc  10012  uzsplit  10023  elfzm1b  10029  elfzp12  10030  fznn0  10044  exfzdc  10171  flqeqceilz  10249  zmodid2  10283  expap0  10481  qsqeqor  10561  bernneq  10571  hasheqf1o  10694  hashfacen  10745  sqrtmsq2i  11073  maxclpr  11160  minmax  11167  xrmaxlesup  11196  xrnegiso  11199  xrnegcon1d  11201  xrminmax  11202  clim0  11222  climrecvg1n  11285  summodc  11320  fsumsplit  11344  mertenslem2  11473  prodmodc  11515  fprodsplitdc  11533  fprod2dlemstep  11559  dvdsval2  11726  odd2np1lem  11805  even2n  11807  divalgb  11858  divalgmod  11860  zsupcllemstep  11874  gcddvds  11892  bezoutlemmain  11927  nnwofdc  11967  isprm3  12046  prmind2  12048  dvdsprime  12050  coprm  12072  prmdvdsexp  12076  sqrt2irr  12090  sqpweven  12103  2sqpwodd  12104  pythagtriplem2  12194  pythagtrip  12211  pceu  12223  pc11  12258  elrest  12558  istopon  12611  isbasis2g  12643  isbasis3g  12644  tgss2  12679  bastop1  12683  iscld  12703  ntreq0  12732  restsn  12780  restopn2  12783  lmbr  12813  cnptoprest2  12840  txbas  12858  eltx  12859  txlm  12879  ishmeo  12904  hmeoimaf1o  12914  ispsmet  12923  ismet  12944  isxmet  12945  ismet2  12954  metn0  12978  elblps  12990  elbl  12991  bdbl  13103  qtopbasss  13121  elcncf  13160  ellimc3apf  13229  sincosq1sgn  13347  sincosq2sgn  13348  cos11  13374  logrpap0b  13397  lgsdir2lem4  13532  2sqlem6  13556  2sqlem9  13560  2sqlem10  13561  subctctexmid  13841  iooref1o  13873  iswomni0  13890