Theorem bitrdi 196

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitrdi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitrdi.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
bitrdi	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitrdi.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	a1i 9	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 188	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

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  6516  brtpos2  6526  brtpos0  6527  rntpos  6532  dftpos3  6537  tpostpos  6539  tpossym  6551  tposoprab  6555  tfrcllemres  6637  frecabcl  6674  frecsuclem  6681  erth2  6858  qliftfun  6895  erovlem  6905  ecopovsym  6909  ecopovsymg  6912  th3qlem1  6915  mapdm0  6941  elpmg  6942  elpm2g  6943  map0e  6971  dom2lem  7063  mapsnend  7104  mapsnen  7105  xpdom2  7134  xpf1o  7149  mapen  7151  ssfilem  7182  ssfilemd  7184  diffitest  7196  ac6sfi  7207  eqsndc  7215  ss1o0el1o  7225  2omap  7325  isoti  7354  cnvti  7366  omp1eomlem  7441  ismkvnex  7502  nninfwlporlemd  7519  en2prde  7546  netap  7627  2omotaplemap  7630  ltexpi  7711  ordpipqqs  7748  ltexnqq  7782  enq0enq  7805  enq0sym  7806  enq0tr  7808  nqnq0pi  7812  genipv  7883  genprndl  7895  genprndu  7896  genpdisj  7897  genpassl  7898  genpassu  7899  addcomprg  7952  mulcomprg  7954  ltnqpr  7967  ltnqpri  7968  ltexprlemm  7974  ltexprlemdisj  7980  suplocexprlemmu  8092  suplocexprlemdisj  8094  ltsrprg  8121  mulgt0sr  8152  elreal2  8204  ltresr  8213  ltresr2  8214  axprecex  8254  axpre-ltadd  8260  axpre-mulgt0  8261  axpre-mulext  8262  axpre-suploclemres  8275  subcan2  8559  negcon1  8586  negcon2  8587  lt0neg1  8804  lt0neg2  8805  le0neg1  8806  le0neg2  8807  reapirr  8914  reapmul1  8932  reapneg  8934  remulext1  8936  apti  8959  negap0  8967  divmulap2  9015  reclt1  9235  recgt1  9236  suprleubex  9293  addltmul  9554  elznn0  9671  zapne  9731  zltlen  9736  nn0lt10b  9738  nn0lt2  9739  eluz1  9942  raluz  9995  rexuz  9997  qltlen  10057  cnref1o  10069  rpnegap  10105  ltxr  10195  xlt0neg1  10258  xlt0neg2  10259  xle0neg1  10260  xle0neg2  10261  elixx1  10317  elixx3g  10321  elioo2  10341  icc0r  10346  elicc4  10360  elioopnf  10387  elioomnf  10388  iooneg  10408  iccneg  10409  iccshftr  10414  iccshftl  10416  iccdil  10418  icccntr  10420  iccf1o  10425  elfz1  10434  0fz1  10467  fzpr  10502  fzdifsuc  10506  uzsplit  10517  elfzm1b  10523  elfzp12  10524  fznn0  10538  exfzdc  10677  zsupcllemstep  10680  flqeqceilz  10777  zmodid2  10811  expap0  11028  qsqeqor  11109  bernneq  11120  hasheqf1o  11247  ssenneg  11303  hashfibclem  11305  hashfacen  11307  hashf1  11310  ccatrn  11400  pfxsuffeqwrdeq  11493  wrd2ind  11518  sqrtmsq2i  11925  maxclpr  12012  minmax  12021  xrmaxlesup  12051  xrnegiso  12054  xrnegcon1d  12056  xrminmax  12057  clim0  12077  climrecvg1n  12140  summodc  12176  fsumsplit  12200  mertenslem2  12329  prodmodc  12371  fprodsplitdc  12389  fprod2dlemstep  12415  dvdsval2  12583  odd2np1lem  12665  even2n  12667  divalgb  12718  divalgmod  12720  bitsval  12736  bitsmod  12749  gcddvds  12766  bezoutlemmain  12801  nnwofdc  12841  isprm3  12922  prmind2  12924  dvdsprime  12926  coprm  12949  prmdvdsexp  12953  sqrt2irr  12967  sqpweven  12981  2sqpwodd  12982  pythagtriplem2  13075  pythagtrip  13092  pceu  13104  pc11  13140  prmlem0  13250  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemodife  13299  elrest  13660  grpsubeq0  13951  grpsubadd  13953  issubg3  14055  isnsg  14065  eqger  14087  eqglact  14088  eqgid  14089  elcntz  14155  elcntzsn  14158  sscntz  14159  idjusnfi  14271  srgfcl  14385  dvdsrtr  14518  dvdsr02  14522  isunitd  14523  isrhm  14575  isrim0  14578  subsubrng2  14633  subsubrg2  14664  issubrg3  14665  opprdomnbg  14693  2idlelb  14952  mplelbascoe  15220  istopon  15251  isbasis2g  15283  isbasis3g  15284  tgss2  15317  bastop1  15321  iscld  15341  ntreq0  15370  restsn  15418  restopn2  15421  lmbr  15451  cnptoprest2  15478  txbas  15496  eltx  15497  txlm  15517  ishmeo  15542  hmeoimaf1o  15552  ispsmet  15561  ismet  15582  isxmet  15583  ismet2  15592  metn0  15616  elblps  15628  elbl  15629  bdbl  15741  qtopbasss  15759  elcncf  15811  ellimc3apf  15898  elply  15972  efap1p  16017  sincosq1sgn  16065  sincosq2sgn  16066  cos11  16093  logrpap0b  16118  lgsdir2lem4  16367  gausslemma2dlem0i  16393  lgsquadlem2  16414  m1lgs  16421  2lgsoddprmlem3  16447  2sqlem6  16456  2sqlem9  16460  2sqlem10  16461  vtxdfifiun  16755  wlkl1loop  16816  wlkv0  16827  wlklenvclwlk  16831  upgr2wlkdc  16835  isclwwlk  16852  isclwwlkng  16864  isclwwlknx  16874  clwwlkn2  16879  eupth2lem2dc  16917  eupth2lem3lem6fi  16929  pw1map  17242  subctctexmid  17247  iooref1o  17301  iswomni0  17320