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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr2di  197  bitr4di  198  3bitr3g  222  bibi2i  227  ibibr  246  biancomd  271  imanst  900  pm5.75  975  xordidc  1448  19.17  1609  alexdc  1672  nf4dc  1722  abeq2d  2351  eqabrd  2378  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvrab  2819  ceqsralt  2849  ralab2  2990  rexab2  2992  euxfr2dc  3011  reu7  3021  reu8  3022  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  ralss  3314  rexss  3315  sseq0b  3564  elif  3652  prssg  3872  2ralunsn  3924  eluniab  3947  elintab  3981  dfiun2g  4044  dfiin2g  4045  cbvopab1  4204  cbvmpt  4226  axsepg  4250  bnd2  4310  opeqsn  4393  reusv3  4606  tfisi  4734  opeliunxp  4830  eliunxp  4919  relop  4930  eldm2g  4977  reldm0  4999  relrn0  5044  restidsing  5119  xpmlem  5208  elxp5  5276  cnvpom  5330  cbviota  5342  iota1  5352  sniota  5368  fncnv  5447  fnres  5500  brprcneu  5688  fnopfvb  5742  fvelrnb  5750  fvelimab  5759  fvopab3g  5778  eqfnfv3  5808  eqfnfv2f  5810  fvreseq  5812  fnreseql  5819  respreima  5836  rexrn  5845  ralrn  5846  f1ompt  5859  fsn  5880  fconstfvm  5933  fconst3m  5934  fconst4m  5935  foima2  5957  rexima  5960  ralima  5961  dff13  5974  foeqcnvco  5996  fliftfun  6002  isocnv  6017  isoini  6024  f1oiso  6032  cbvriota  6050  riotaeqimp  6063  eusvobj2  6071  oprabid  6117  eloprabga  6175  resoprab  6184  eqfnov  6195  eqfnov2  6196  ov6g  6227  funimassov  6239  ovelimab  6240  caovord2  6262  uchoice  6371  releldm2  6419  dfoprab4  6426  xporderlem  6467  poxp  6468  f1od2  6471  elsuppfng  6482  elsuppfn  6483  rexsupp  6493  mpoxopovel  6512  brtpos2  6522  brtpos0  6523  rntpos  6528  dftpos3  6533  tpostpos  6535  tpossym  6547  tposoprab  6551  tfrcllemres  6633  frecabcl  6670  frecsuclem  6677  erth2  6854  qliftfun  6891  erovlem  6901  ecopovsym  6905  ecopovsymg  6908  th3qlem1  6911  mapdm0  6937  elpmg  6938  elpm2g  6939  map0e  6967  dom2lem  7058  mapsnend  7099  mapsnen  7100  xpdom2  7129  xpf1o  7144  mapen  7146  ssfilem  7177  ssfilemd  7179  diffitest  7191  ac6sfi  7202  eqsndc  7210  ss1o0el1o  7220  2omap  7318  isoti  7347  cnvti  7359  omp1eomlem  7434  ismkvnex  7495  nninfwlporlemd  7512  en2prde  7539  netap  7620  2omotaplemap  7623  ltexpi  7704  ordpipqqs  7741  ltexnqq  7775  enq0enq  7798  enq0sym  7799  enq0tr  7801  nqnq0pi  7805  genipv  7876  genprndl  7888  genprndu  7889  genpdisj  7890  genpassl  7891  genpassu  7892  addcomprg  7945  mulcomprg  7947  ltnqpr  7960  ltnqpri  7961  ltexprlemm  7967  ltexprlemdisj  7973  suplocexprlemmu  8085  suplocexprlemdisj  8087  ltsrprg  8114  mulgt0sr  8145  elreal2  8197  ltresr  8206  ltresr2  8207  axprecex  8247  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axpre-suploclemres  8268  subcan2  8552  negcon1  8579  negcon2  8580  lt0neg1  8797  lt0neg2  8798  le0neg1  8799  le0neg2  8800  reapirr  8907  reapmul1  8925  reapneg  8927  remulext1  8929  apti  8952  negap0  8960  divmulap2  9008  reclt1  9228  recgt1  9229  suprleubex  9286  addltmul  9546  elznn0  9663  zapne  9723  zltlen  9728  nn0lt10b  9730  nn0lt2  9731  eluz1  9934  raluz  9987  rexuz  9989  qltlen  10049  cnref1o  10061  rpnegap  10097  ltxr  10187  xlt0neg1  10250  xlt0neg2  10251  xle0neg1  10252  xle0neg2  10253  elixx1  10309  elixx3g  10313  elioo2  10333  icc0r  10338  elicc4  10352  elioopnf  10379  elioomnf  10380  iooneg  10400  iccneg  10401  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  iccf1o  10417  elfz1  10426  0fz1  10459  fzpr  10494  fzdifsuc  10498  uzsplit  10509  elfzm1b  10515  elfzp12  10516  fznn0  10530  exfzdc  10669  zsupcllemstep  10672  flqeqceilz  10768  zmodid2  10802  expap0  11019  qsqeqor  11100  bernneq  11111  hasheqf1o  11238  ssenneg  11294  hashfibclem  11296  hashfacen  11298  hashf1  11301  ccatrn  11391  pfxsuffeqwrdeq  11484  wrd2ind  11509  sqrtmsq2i  11916  maxclpr  12003  minmax  12011  xrmaxlesup  12041  xrnegiso  12044  xrnegcon1d  12046  xrminmax  12047  clim0  12067  climrecvg1n  12130  summodc  12166  fsumsplit  12190  mertenslem2  12319  prodmodc  12361  fprodsplitdc  12379  fprod2dlemstep  12405  dvdsval2  12573  odd2np1lem  12655  even2n  12657  divalgb  12708  divalgmod  12710  bitsval  12726  bitsmod  12739  gcddvds  12756  bezoutlemmain  12791  nnwofdc  12831  isprm3  12912  prmind2  12914  dvdsprime  12916  coprm  12939  prmdvdsexp  12943  sqrt2irr  12957  sqpweven  12971  2sqpwodd  12972  pythagtriplem2  13065  pythagtrip  13082  pceu  13094  pc11  13130  prmlem0  13240  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemodife  13289  elrest  13649  grpsubeq0  13940  grpsubadd  13942  issubg3  14044  isnsg  14054  eqger  14076  eqglact  14077  eqgid  14078  srgfcl  14326  dvdsrtr  14457  dvdsr02  14461  isunitd  14462  isrhm  14514  isrim0  14517  subsubrng2  14572  subsubrg2  14603  issubrg3  14604  opprdomnbg  14632  2idlelb  14891  mplelbascoe  15132  istopon  15163  isbasis2g  15195  isbasis3g  15196  tgss2  15229  bastop1  15233  iscld  15253  ntreq0  15282  restsn  15330  restopn2  15333  lmbr  15363  cnptoprest2  15390  txbas  15408  eltx  15409  txlm  15429  ishmeo  15454  hmeoimaf1o  15464  ispsmet  15473  ismet  15494  isxmet  15495  ismet2  15504  metn0  15528  elblps  15540  elbl  15541  bdbl  15653  qtopbasss  15671  elcncf  15723  ellimc3apf  15810  elply  15884  efap1p  15929  sincosq1sgn  15977  sincosq2sgn  15978  cos11  16004  logrpap0b  16028  lgsdir2lem4  16248  gausslemma2dlem0i  16274  lgsquadlem2  16295  m1lgs  16302  2lgsoddprmlem3  16328  2sqlem6  16337  2sqlem9  16341  2sqlem10  16342  vtxdfifiun  16636  wlkl1loop  16697  wlkv0  16708  wlklenvclwlk  16712  upgr2wlkdc  16716  isclwwlk  16733  isclwwlkng  16745  isclwwlknx  16755  clwwlkn2  16760  eupth2lem2dc  16798  eupth2lem3lem6fi  16810  pw1map  17123  subctctexmid  17128  iooref1o  17181  iswomni0  17199