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  4205  cbvmpt  4228  axsepg  4252  bnd2  4312  opeqsn  4395  reusv3  4608  tfisi  4736  opeliunxp  4832  eliunxp  4921  relop  4932  eldm2g  4979  reldm0  5001  relrn0  5046  restidsing  5122  xpmlem  5211  elxp5  5279  cnvpom  5333  cbviota  5345  iota1  5355  sniota  5371  fncnv  5450  fnres  5503  brprcneu  5691  fnopfvb  5745  fvelrnb  5753  fvelimab  5762  fvopab3g  5781  eqfnfv3  5811  eqfnfv2f  5813  fvreseq  5815  fnreseql  5822  respreima  5839  rexrn  5848  ralrn  5849  f1ompt  5862  fsn  5883  fconstfvm  5936  fconst3m  5937  fconst4m  5938  foima2  5960  rexima  5963  ralima  5964  dff13  5977  foeqcnvco  5999  fliftfun  6005  isocnv  6020  isoini  6027  f1oiso  6035  cbvriota  6053  riotaeqimp  6066  eusvobj2  6074  oprabid  6120  eloprabga  6178  resoprab  6187  eqfnov  6198  eqfnov2  6199  ov6g  6230  funimassov  6242  ovelimab  6243  caovord2  6265  uchoice  6375  releldm2  6423  dfoprab4  6430  xporderlem  6471  poxp  6472  f1od2  6475  elsuppfng  6486  elsuppfn  6487  rexsupp  6497  mpoxopovel  6517  brtpos2  6527  brtpos0  6528  rntpos  6533  dftpos3  6538  tpostpos  6540  tpossym  6552  tposoprab  6556  tfrcllemres  6638  frecabcl  6675  frecsuclem  6682  erth2  6859  qliftfun  6896  erovlem  6906  ecopovsym  6910  ecopovsymg  6913  th3qlem1  6916  mapdm0  6942  elpmg  6943  elpm2g  6944  map0e  6972  dom2lem  7064  mapsnend  7105  mapsnen  7106  xpdom2  7135  xpf1o  7150  mapen  7152  ssfilem  7183  ssfilemd  7185  diffitest  7197  ac6sfi  7208  eqsndc  7216  ss1o0el1o  7226  2omap  7324  isoti  7353  cnvti  7365  omp1eomlem  7440  ismkvnex  7501  nninfwlporlemd  7518  en2prde  7545  netap  7626  2omotaplemap  7629  ltexpi  7710  ordpipqqs  7747  ltexnqq  7781  enq0enq  7804  enq0sym  7805  enq0tr  7807  nqnq0pi  7811  genipv  7882  genprndl  7894  genprndu  7895  genpdisj  7896  genpassl  7897  genpassu  7898  addcomprg  7951  mulcomprg  7953  ltnqpr  7966  ltnqpri  7967  ltexprlemm  7973  ltexprlemdisj  7979  suplocexprlemmu  8091  suplocexprlemdisj  8093  ltsrprg  8120  mulgt0sr  8151  elreal2  8203  ltresr  8212  ltresr2  8213  axprecex  8253  axpre-ltadd  8259  axpre-mulgt0  8260  axpre-mulext  8261  axpre-suploclemres  8274  subcan2  8558  negcon1  8585  negcon2  8586  lt0neg1  8803  lt0neg2  8804  le0neg1  8805  le0neg2  8806  reapirr  8913  reapmul1  8931  reapneg  8933  remulext1  8935  apti  8958  negap0  8966  divmulap2  9014  reclt1  9234  recgt1  9235  suprleubex  9292  addltmul  9553  elznn0  9668  zapne  9728  zltlen  9733  nn0lt10b  9735  nn0lt2  9736  eluz1  9940  raluz  9993  rexuz  9995  qltlen  10055  cnref1o  10067  rpnegap  10103  ltxr  10193  xlt0neg1  10256  xlt0neg2  10257  xle0neg1  10258  xle0neg2  10259  elixx1  10315  elixx3g  10319  elioo2  10339  icc0r  10344  elicc4  10358  elioopnf  10385  elioomnf  10386  iooneg  10406  iccneg  10407  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  iccf1o  10423  elfz1  10432  0fz1  10465  fzpr  10500  fzdifsuc  10504  uzsplit  10515  elfzm1b  10521  elfzp12  10522  fznn0  10536  exfzdc  10675  zsupcllemstep  10678  flqeqceilz  10775  zmodid2  10809  expap0  11026  qsqeqor  11107  bernneq  11118  hasheqf1o  11245  ssenneg  11301  hashfibclem  11303  hashfacen  11305  hashf1  11308  ccatrn  11398  pfxsuffeqwrdeq  11491  wrd2ind  11516  sqrtmsq2i  11923  maxclpr  12010  minmax  12019  xrmaxlesup  12049  xrnegiso  12052  xrnegcon1d  12054  xrminmax  12055  clim0  12075  climrecvg1n  12138  summodc  12174  fsumsplit  12198  mertenslem2  12327  prodmodc  12369  fprodsplitdc  12387  fprod2dlemstep  12413  dvdsval2  12581  odd2np1lem  12663  even2n  12665  divalgb  12716  divalgmod  12718  bitsval  12734  bitsmod  12747  gcddvds  12764  bezoutlemmain  12799  nnwofdc  12839  isprm3  12920  prmind2  12922  dvdsprime  12924  coprm  12947  prmdvdsexp  12951  sqrt2irr  12965  sqpweven  12979  2sqpwodd  12980  pythagtriplem2  13073  pythagtrip  13090  pceu  13102  pc11  13138  prmlem0  13248  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemodife  13297  elrest  13658  grpsubeq0  13949  grpsubadd  13951  issubg3  14053  isnsg  14063  eqger  14085  eqglact  14086  eqgid  14087  elcntz  14153  elcntzsn  14156  sscntz  14157  idjusnfi  14269  srgfcl  14383  dvdsrtr  14516  dvdsr02  14520  isunitd  14521  isrhm  14573  isrim0  14576  subsubrng2  14631  subsubrg2  14662  issubrg3  14663  opprdomnbg  14691  2idlelb  14950  istopon  15256  isbasis2g  15288  isbasis3g  15289  tgss2  15322  bastop1  15326  iscld  15346  ntreq0  15375  restsn  15423  restopn2  15426  lmbr  15456  cnptoprest2  15483  txbas  15501  eltx  15502  txlm  15522  ishmeo  15547  hmeoimaf1o  15557  ispsmet  15566  ismet  15587  isxmet  15588  ismet2  15597  metn0  15621  elblps  15633  elbl  15634  bdbl  15746  qtopbasss  15764  elcncf  15816  ellimc3apf  15903  elply  15977  efap1p  16022  sincosq1sgn  16070  sincosq2sgn  16071  cos11  16098  logrpap0b  16123  lgsdir2lem4  16372  gausslemma2dlem0i  16398  lgsquadlem2  16419  m1lgs  16426  2lgsoddprmlem3  16452  2sqlem6  16461  2sqlem9  16465  2sqlem10  16466  vtxdfifiun  16760  wlkl1loop  16821  wlkv0  16832  wlklenvclwlk  16836  upgr2wlkdc  16840  isclwwlk  16857  isclwwlkng  16869  isclwwlknx  16879  clwwlkn2  16884  eupth2lem2dc  16922  eupth2lem3lem6fi  16934  pw1map  17247  subctctexmid  17252  iooref1o  17306  iswomni0  17325