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  893  pm5.75  968  xordidc  1441  19.17  1602  alexdc  1665  nf4dc  1716  abeq2d  2342  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvrab  2797  ceqsralt  2827  ralab2  2967  rexab2  2969  euxfr2dc  2988  reu7  2998  reu8  2999  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  ralss  3290  rexss  3291  elif  3614  prssg  3824  2ralunsn  3876  eluniab  3899  elintab  3933  dfiun2g  3996  dfiin2g  3997  cbvopab1  4156  cbvmpt  4178  axsep2  4202  bnd2  4256  opeqsn  4338  reusv3  4550  tfisi  4678  opeliunxp  4773  eliunxp  4860  relop  4871  eldm2g  4918  reldm0  4940  relrn0  4985  restidsing  5060  xpmlem  5148  elxp5  5216  cnvpom  5270  cbviota  5282  iota1  5292  sniota  5308  fncnv  5386  fnres  5439  brprcneu  5619  fnopfvb  5672  fvelrnb  5680  fvelimab  5689  fvopab3g  5706  eqfnfv3  5733  eqfnfv2f  5735  fvreseq  5737  fnreseql  5744  rexsupp  5758  respreima  5762  rexrn  5771  ralrn  5772  f1ompt  5785  fsn  5806  fconstfvm  5856  fconst3m  5857  fconst4m  5858  foima2  5874  rexima  5877  ralima  5878  dff13  5891  foeqcnvco  5913  fliftfun  5919  isocnv  5934  isoini  5941  f1oiso  5949  cbvriota  5965  riotaeqimp  5978  eusvobj2  5986  oprabid  6032  eloprabga  6090  resoprab  6099  eqfnov  6110  eqfnov2  6111  ov6g  6142  funimassov  6154  ovelimab  6155  caovord2  6177  uchoice  6281  releldm2  6329  dfoprab4  6336  xporderlem  6375  poxp  6376  f1od2  6379  mpoxopovel  6385  brtpos2  6395  brtpos0  6396  rntpos  6401  dftpos3  6406  tpostpos  6408  tpossym  6420  tposoprab  6424  tfrcllemres  6506  frecabcl  6543  frecsuclem  6550  erth2  6725  qliftfun  6762  erovlem  6772  ecopovsym  6776  ecopovsymg  6779  th3qlem1  6782  mapdm0  6808  elpmg  6809  elpm2g  6810  map0e  6831  dom2lem  6921  mapsnen  6962  xpdom2  6986  xpf1o  7001  mapen  7003  ssfilem  7033  diffitest  7045  ac6sfi  7056  ss1o0el1o  7071  isoti  7170  cnvti  7182  omp1eomlem  7257  ismkvnex  7318  nninfwlporlemd  7335  en2prde  7362  netap  7436  2omotaplemap  7439  ltexpi  7520  ordpipqqs  7557  ltexnqq  7591  enq0enq  7614  enq0sym  7615  enq0tr  7617  nqnq0pi  7621  genipv  7692  genprndl  7704  genprndu  7705  genpdisj  7706  genpassl  7707  genpassu  7708  addcomprg  7761  mulcomprg  7763  ltnqpr  7776  ltnqpri  7777  ltexprlemm  7783  ltexprlemdisj  7789  suplocexprlemmu  7901  suplocexprlemdisj  7903  ltsrprg  7930  mulgt0sr  7961  elreal2  8013  ltresr  8022  ltresr2  8023  axprecex  8063  axpre-ltadd  8069  axpre-mulgt0  8070  axpre-mulext  8071  axpre-suploclemres  8084  subcan2  8367  negcon1  8394  negcon2  8395  lt0neg1  8611  lt0neg2  8612  le0neg1  8613  le0neg2  8614  reapirr  8720  reapmul1  8738  reapneg  8740  remulext1  8742  apti  8765  negap0  8773  divmulap2  8819  reclt1  9039  recgt1  9040  suprleubex  9097  addltmul  9344  elznn0  9457  zapne  9517  zltlen  9521  nn0lt10b  9523  nn0lt2  9524  eluz1  9722  raluz  9769  rexuz  9771  qltlen  9831  cnref1o  9842  rpnegap  9878  ltxr  9967  xlt0neg1  10030  xlt0neg2  10031  xle0neg1  10032  xle0neg2  10033  elixx1  10089  elixx3g  10093  elioo2  10113  icc0r  10118  elicc4  10132  elioopnf  10159  elioomnf  10160  iooneg  10180  iccneg  10181  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  iccf1o  10196  elfz1  10205  0fz1  10237  fzpr  10269  fzdifsuc  10273  uzsplit  10284  elfzm1b  10290  elfzp12  10291  fznn0  10305  exfzdc  10441  zsupcllemstep  10444  flqeqceilz  10535  zmodid2  10569  expap0  10786  qsqeqor  10867  bernneq  10877  hasheqf1o  11002  hashfacen  11053  ccatrn  11139  pfxsuffeqwrdeq  11225  wrd2ind  11250  sqrtmsq2i  11641  maxclpr  11728  minmax  11736  xrmaxlesup  11765  xrnegiso  11768  xrnegcon1d  11770  xrminmax  11771  clim0  11791  climrecvg1n  11854  summodc  11889  fsumsplit  11913  mertenslem2  12042  prodmodc  12084  fprodsplitdc  12102  fprod2dlemstep  12128  dvdsval2  12296  odd2np1lem  12378  even2n  12380  divalgb  12431  divalgmod  12433  bitsval  12449  bitsmod  12462  gcddvds  12479  bezoutlemmain  12514  nnwofdc  12554  isprm3  12635  prmind2  12637  dvdsprime  12639  coprm  12661  prmdvdsexp  12665  sqrt2irr  12679  sqpweven  12692  2sqpwodd  12693  pythagtriplem2  12784  pythagtrip  12801  pceu  12813  pc11  12849  elrest  13274  grpsubeq0  13614  grpsubadd  13616  issubg3  13724  isnsg  13734  eqger  13756  eqglact  13757  eqgid  13758  srgfcl  13931  dvdsrtr  14059  dvdsr02  14063  isunitd  14064  isrhm  14116  isrim0  14119  subsubrng2  14173  subsubrg2  14204  issubrg3  14205  opprdomnbg  14232  2idlelb  14463  mplelbascoe  14650  istopon  14681  isbasis2g  14713  isbasis3g  14714  tgss2  14747  bastop1  14751  iscld  14771  ntreq0  14800  restsn  14848  restopn2  14851  lmbr  14881  cnptoprest2  14908  txbas  14926  eltx  14927  txlm  14947  ishmeo  14972  hmeoimaf1o  14982  ispsmet  14991  ismet  15012  isxmet  15013  ismet2  15022  metn0  15046  elblps  15058  elbl  15059  bdbl  15171  qtopbasss  15189  elcncf  15241  ellimc3apf  15328  elply  15402  sincosq1sgn  15494  sincosq2sgn  15495  cos11  15521  logrpap0b  15544  lgsdir2lem4  15704  gausslemma2dlem0i  15730  lgsquadlem2  15751  m1lgs  15758  2lgsoddprmlem3  15784  2sqlem6  15793  2sqlem9  15797  2sqlem10  15798  2omap  16318  pw1map  16320  subctctexmid  16325  iooref1o  16361  iswomni0  16378