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  889  pm5.75  964  xordidc  1410  19.17  1570  alexdc  1633  nf4dc  1684  abeq2d  2309  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvrab  2761  ceqsralt  2790  ralab2  2928  rexab2  2930  euxfr2dc  2949  reu7  2959  reu8  2960  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  ralss  3249  rexss  3250  prssg  3779  2ralunsn  3828  eluniab  3851  elintab  3885  dfiun2g  3948  dfiin2g  3949  cbvopab1  4106  cbvmpt  4128  axsep2  4152  bnd2  4206  opeqsn  4285  reusv3  4495  tfisi  4623  opeliunxp  4718  eliunxp  4805  relop  4816  eldm2g  4862  reldm0  4884  relrn0  4928  restidsing  5002  xpmlem  5090  elxp5  5158  cnvpom  5212  cbviota  5224  iota1  5233  sniota  5249  fncnv  5324  fnres  5374  brprcneu  5551  fnopfvb  5602  fvelrnb  5608  fvelimab  5617  fvopab3g  5634  eqfnfv3  5661  eqfnfv2f  5663  fvreseq  5665  fnreseql  5672  rexsupp  5686  respreima  5690  rexrn  5699  ralrn  5700  f1ompt  5713  fsn  5734  fconstfvm  5780  fconst3m  5781  fconst4m  5782  foima2  5798  rexima  5801  ralima  5802  dff13  5815  foeqcnvco  5837  fliftfun  5843  isocnv  5858  isoini  5865  f1oiso  5873  cbvriota  5888  eusvobj2  5908  oprabid  5954  eloprabga  6009  resoprab  6018  eqfnov  6029  eqfnov2  6030  ov6g  6061  funimassov  6073  ovelimab  6074  caovord2  6096  uchoice  6195  releldm2  6243  dfoprab4  6250  xporderlem  6289  poxp  6290  f1od2  6293  mpoxopovel  6299  brtpos2  6309  brtpos0  6310  rntpos  6315  dftpos3  6320  tpostpos  6322  tpossym  6334  tposoprab  6338  tfrcllemres  6420  frecabcl  6457  frecsuclem  6464  erth2  6639  qliftfun  6676  erovlem  6686  ecopovsym  6690  ecopovsymg  6693  th3qlem1  6696  mapdm0  6722  elpmg  6723  elpm2g  6724  map0e  6745  dom2lem  6831  mapsnen  6870  xpdom2  6890  xpf1o  6905  mapen  6907  ssfilem  6936  diffitest  6948  ac6sfi  6959  ss1o0el1o  6974  isoti  7073  cnvti  7085  omp1eomlem  7160  ismkvnex  7221  nninfwlporlemd  7238  netap  7321  2omotaplemap  7324  ltexpi  7404  ordpipqqs  7441  ltexnqq  7475  enq0enq  7498  enq0sym  7499  enq0tr  7501  nqnq0pi  7505  genipv  7576  genprndl  7588  genprndu  7589  genpdisj  7590  genpassl  7591  genpassu  7592  addcomprg  7645  mulcomprg  7647  ltnqpr  7660  ltnqpri  7661  ltexprlemm  7667  ltexprlemdisj  7673  suplocexprlemmu  7785  suplocexprlemdisj  7787  ltsrprg  7814  mulgt0sr  7845  elreal2  7897  ltresr  7906  ltresr2  7907  axprecex  7947  axpre-ltadd  7953  axpre-mulgt0  7954  axpre-mulext  7955  axpre-suploclemres  7968  subcan2  8251  negcon1  8278  negcon2  8279  lt0neg1  8495  lt0neg2  8496  le0neg1  8497  le0neg2  8498  reapirr  8604  reapmul1  8622  reapneg  8624  remulext1  8626  apti  8649  negap0  8657  divmulap2  8703  reclt1  8923  recgt1  8924  suprleubex  8981  addltmul  9228  elznn0  9341  zapne  9400  zltlen  9404  nn0lt10b  9406  nn0lt2  9407  eluz1  9605  raluz  9652  rexuz  9654  qltlen  9714  cnref1o  9725  rpnegap  9761  ltxr  9850  xlt0neg1  9913  xlt0neg2  9914  xle0neg1  9915  xle0neg2  9916  elixx1  9972  elixx3g  9976  elioo2  9996  icc0r  10001  elicc4  10015  elioopnf  10042  elioomnf  10043  iooneg  10063  iccneg  10064  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  iccf1o  10079  elfz1  10088  0fz1  10120  fzpr  10152  fzdifsuc  10156  uzsplit  10167  elfzm1b  10173  elfzp12  10174  fznn0  10188  exfzdc  10316  zsupcllemstep  10319  flqeqceilz  10410  zmodid2  10444  expap0  10661  qsqeqor  10742  bernneq  10752  hasheqf1o  10877  hashfacen  10928  sqrtmsq2i  11300  maxclpr  11387  minmax  11395  xrmaxlesup  11424  xrnegiso  11427  xrnegcon1d  11429  xrminmax  11430  clim0  11450  climrecvg1n  11513  summodc  11548  fsumsplit  11572  mertenslem2  11701  prodmodc  11743  fprodsplitdc  11761  fprod2dlemstep  11787  dvdsval2  11955  odd2np1lem  12037  even2n  12039  divalgb  12090  divalgmod  12092  bitsval  12108  gcddvds  12130  bezoutlemmain  12165  nnwofdc  12205  isprm3  12286  prmind2  12288  dvdsprime  12290  coprm  12312  prmdvdsexp  12316  sqrt2irr  12330  sqpweven  12343  2sqpwodd  12344  pythagtriplem2  12435  pythagtrip  12452  pceu  12464  pc11  12500  elrest  12917  grpsubeq0  13218  grpsubadd  13220  issubg3  13322  isnsg  13332  eqger  13354  eqglact  13355  eqgid  13356  srgfcl  13529  dvdsrtr  13657  dvdsr02  13661  isunitd  13662  isrhm  13714  isrim0  13717  subsubrng2  13771  subsubrg2  13802  issubrg3  13803  opprdomnbg  13830  2idlelb  14061  istopon  14249  isbasis2g  14281  isbasis3g  14282  tgss2  14315  bastop1  14319  iscld  14339  ntreq0  14368  restsn  14416  restopn2  14419  lmbr  14449  cnptoprest2  14476  txbas  14494  eltx  14495  txlm  14515  ishmeo  14540  hmeoimaf1o  14550  ispsmet  14559  ismet  14580  isxmet  14581  ismet2  14590  metn0  14614  elblps  14626  elbl  14627  bdbl  14739  qtopbasss  14757  elcncf  14809  ellimc3apf  14896  elply  14970  sincosq1sgn  15062  sincosq2sgn  15063  cos11  15089  logrpap0b  15112  lgsdir2lem4  15272  gausslemma2dlem0i  15298  lgsquadlem2  15319  m1lgs  15326  2lgsoddprmlem3  15352  2sqlem6  15361  2sqlem9  15365  2sqlem10  15366  subctctexmid  15645  iooref1o  15678  iswomni0  15695