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  8551  negcon1  8578  negcon2  8579  lt0neg1  8796  lt0neg2  8797  le0neg1  8798  le0neg2  8799  reapirr  8905  reapmul1  8923  reapneg  8925  remulext1  8927  apti  8950  negap0  8958  divmulap2  9006  reclt1  9226  recgt1  9227  suprleubex  9284  addltmul  9542  elznn0  9659  zapne  9719  zltlen  9724  nn0lt10b  9726  nn0lt2  9727  eluz1  9925  raluz  9978  rexuz  9980  qltlen  10040  cnref1o  10051  rpnegap  10087  ltxr  10177  xlt0neg1  10240  xlt0neg2  10241  xle0neg1  10242  xle0neg2  10243  elixx1  10299  elixx3g  10303  elioo2  10323  icc0r  10328  elicc4  10342  elioopnf  10369  elioomnf  10370  iooneg  10390  iccneg  10391  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  iccf1o  10407  elfz1  10416  0fz1  10449  fzpr  10484  fzdifsuc  10488  uzsplit  10499  elfzm1b  10505  elfzp12  10506  fznn0  10520  exfzdc  10659  zsupcllemstep  10662  flqeqceilz  10755  zmodid2  10789  expap0  11006  qsqeqor  11087  bernneq  11098  hasheqf1o  11224  ssenneg  11280  hashfibclem  11282  hashfacen  11284  hashf1  11287  ccatrn  11377  pfxsuffeqwrdeq  11470  wrd2ind  11495  sqrtmsq2i  11901  maxclpr  11988  minmax  11996  xrmaxlesup  12025  xrnegiso  12028  xrnegcon1d  12030  xrminmax  12031  clim0  12051  climrecvg1n  12114  summodc  12150  fsumsplit  12174  mertenslem2  12303  prodmodc  12345  fprodsplitdc  12363  fprod2dlemstep  12389  dvdsval2  12557  odd2np1lem  12639  even2n  12641  divalgb  12692  divalgmod  12694  bitsval  12710  bitsmod  12723  gcddvds  12740  bezoutlemmain  12775  nnwofdc  12815  isprm3  12896  prmind2  12898  dvdsprime  12900  coprm  12922  prmdvdsexp  12926  sqrt2irr  12940  sqpweven  12953  2sqpwodd  12954  pythagtriplem2  13045  pythagtrip  13062  pceu  13074  pc11  13110  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemodife  13240  elrest  13600  grpsubeq0  13891  grpsubadd  13893  issubg3  13995  isnsg  14005  eqger  14027  eqglact  14028  eqgid  14029  srgfcl  14277  dvdsrtr  14408  dvdsr02  14412  isunitd  14413  isrhm  14465  isrim0  14468  subsubrng2  14523  subsubrg2  14554  issubrg3  14555  opprdomnbg  14583  2idlelb  14842  mplelbascoe  15083  istopon  15114  isbasis2g  15146  isbasis3g  15147  tgss2  15180  bastop1  15184  iscld  15204  ntreq0  15233  restsn  15281  restopn2  15284  lmbr  15314  cnptoprest2  15341  txbas  15359  eltx  15360  txlm  15380  ishmeo  15405  hmeoimaf1o  15415  ispsmet  15424  ismet  15445  isxmet  15446  ismet2  15455  metn0  15479  elblps  15491  elbl  15492  bdbl  15604  qtopbasss  15622  elcncf  15674  ellimc3apf  15761  elply  15835  sincosq1sgn  15927  sincosq2sgn  15928  cos11  15954  logrpap0b  15977  lgsdir2lem4  16150  gausslemma2dlem0i  16176  lgsquadlem2  16197  m1lgs  16204  2lgsoddprmlem3  16230  2sqlem6  16239  2sqlem9  16243  2sqlem10  16244  vtxdfifiun  16538  wlkl1loop  16599  wlkv0  16610  wlklenvclwlk  16614  upgr2wlkdc  16618  isclwwlk  16635  isclwwlkng  16647  isclwwlknx  16657  clwwlkn2  16662  eupth2lem2dc  16700  eupth2lem3lem6fi  16712  pw1map  17025  subctctexmid  17030  iooref1o  17083  iswomni0  17101