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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

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  2798  ceqsralt  2828  ralab2  2968  rexab2  2970  euxfr2dc  2989  reu7  2999  reu8  3000  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  ralss  3291  rexss  3292  elif  3615  prssg  3828  2ralunsn  3880  eluniab  3903  elintab  3937  dfiun2g  4000  dfiin2g  4001  cbvopab1  4160  cbvmpt  4182  axsep2  4206  bnd2  4261  opeqsn  4343  reusv3  4555  tfisi  4683  opeliunxp  4779  eliunxp  4867  relop  4878  eldm2g  4925  reldm0  4947  relrn0  4992  restidsing  5067  xpmlem  5155  elxp5  5223  cnvpom  5277  cbviota  5289  iota1  5299  sniota  5315  fncnv  5393  fnres  5446  brprcneu  5628  fnopfvb  5681  fvelrnb  5689  fvelimab  5698  fvopab3g  5715  eqfnfv3  5742  eqfnfv2f  5744  fvreseq  5746  fnreseql  5753  rexsupp  5767  respreima  5771  rexrn  5780  ralrn  5781  f1ompt  5794  fsn  5815  fconstfvm  5867  fconst3m  5868  fconst4m  5869  foima2  5887  rexima  5890  ralima  5891  dff13  5904  foeqcnvco  5926  fliftfun  5932  isocnv  5947  isoini  5954  f1oiso  5962  cbvriota  5978  riotaeqimp  5991  eusvobj2  5999  oprabid  6045  eloprabga  6103  resoprab  6112  eqfnov  6123  eqfnov2  6124  ov6g  6155  funimassov  6167  ovelimab  6168  caovord2  6190  uchoice  6295  releldm2  6343  dfoprab4  6350  xporderlem  6391  poxp  6392  f1od2  6395  mpoxopovel  6402  brtpos2  6412  brtpos0  6413  rntpos  6418  dftpos3  6423  tpostpos  6425  tpossym  6437  tposoprab  6441  tfrcllemres  6523  frecabcl  6560  frecsuclem  6567  erth2  6744  qliftfun  6781  erovlem  6791  ecopovsym  6795  ecopovsymg  6798  th3qlem1  6801  mapdm0  6827  elpmg  6828  elpm2g  6829  map0e  6850  dom2lem  6940  mapsnen  6981  xpdom2  7010  xpf1o  7025  mapen  7027  ssfilem  7057  ssfilemd  7059  diffitest  7071  ac6sfi  7082  eqsndc  7090  ss1o0el1o  7100  isoti  7200  cnvti  7212  omp1eomlem  7287  ismkvnex  7348  nninfwlporlemd  7365  en2prde  7392  netap  7466  2omotaplemap  7469  ltexpi  7550  ordpipqqs  7587  ltexnqq  7621  enq0enq  7644  enq0sym  7645  enq0tr  7647  nqnq0pi  7651  genipv  7722  genprndl  7734  genprndu  7735  genpdisj  7736  genpassl  7737  genpassu  7738  addcomprg  7791  mulcomprg  7793  ltnqpr  7806  ltnqpri  7807  ltexprlemm  7813  ltexprlemdisj  7819  suplocexprlemmu  7931  suplocexprlemdisj  7933  ltsrprg  7960  mulgt0sr  7991  elreal2  8043  ltresr  8052  ltresr2  8053  axprecex  8093  axpre-ltadd  8099  axpre-mulgt0  8100  axpre-mulext  8101  axpre-suploclemres  8114  subcan2  8397  negcon1  8424  negcon2  8425  lt0neg1  8641  lt0neg2  8642  le0neg1  8643  le0neg2  8644  reapirr  8750  reapmul1  8768  reapneg  8770  remulext1  8772  apti  8795  negap0  8803  divmulap2  8849  reclt1  9069  recgt1  9070  suprleubex  9127  addltmul  9374  elznn0  9487  zapne  9547  zltlen  9551  nn0lt10b  9553  nn0lt2  9554  eluz1  9752  raluz  9805  rexuz  9807  qltlen  9867  cnref1o  9878  rpnegap  9914  ltxr  10003  xlt0neg1  10066  xlt0neg2  10067  xle0neg1  10068  xle0neg2  10069  elixx1  10125  elixx3g  10129  elioo2  10149  icc0r  10154  elicc4  10168  elioopnf  10195  elioomnf  10196  iooneg  10216  iccneg  10217  iccshftr  10222  iccshftl  10224  iccdil  10226  icccntr  10228  iccf1o  10232  elfz1  10241  0fz1  10273  fzpr  10305  fzdifsuc  10309  uzsplit  10320  elfzm1b  10326  elfzp12  10327  fznn0  10341  exfzdc  10479  zsupcllemstep  10482  flqeqceilz  10573  zmodid2  10607  expap0  10824  qsqeqor  10905  bernneq  10915  hasheqf1o  11040  hashfacen  11093  ccatrn  11179  pfxsuffeqwrdeq  11272  wrd2ind  11297  sqrtmsq2i  11689  maxclpr  11776  minmax  11784  xrmaxlesup  11813  xrnegiso  11816  xrnegcon1d  11818  xrminmax  11819  clim0  11839  climrecvg1n  11902  summodc  11937  fsumsplit  11961  mertenslem2  12090  prodmodc  12132  fprodsplitdc  12150  fprod2dlemstep  12176  dvdsval2  12344  odd2np1lem  12426  even2n  12428  divalgb  12479  divalgmod  12481  bitsval  12497  bitsmod  12510  gcddvds  12527  bezoutlemmain  12562  nnwofdc  12602  isprm3  12683  prmind2  12685  dvdsprime  12687  coprm  12709  prmdvdsexp  12713  sqrt2irr  12727  sqpweven  12740  2sqpwodd  12741  pythagtriplem2  12832  pythagtrip  12849  pceu  12861  pc11  12897  elrest  13322  grpsubeq0  13662  grpsubadd  13664  issubg3  13772  isnsg  13782  eqger  13804  eqglact  13805  eqgid  13806  srgfcl  13979  dvdsrtr  14108  dvdsr02  14112  isunitd  14113  isrhm  14165  isrim0  14168  subsubrng2  14222  subsubrg2  14253  issubrg3  14254  opprdomnbg  14281  2idlelb  14512  mplelbascoe  14699  istopon  14730  isbasis2g  14762  isbasis3g  14763  tgss2  14796  bastop1  14800  iscld  14820  ntreq0  14849  restsn  14897  restopn2  14900  lmbr  14930  cnptoprest2  14957  txbas  14975  eltx  14976  txlm  14996  ishmeo  15021  hmeoimaf1o  15031  ispsmet  15040  ismet  15061  isxmet  15062  ismet2  15071  metn0  15095  elblps  15107  elbl  15108  bdbl  15220  qtopbasss  15238  elcncf  15290  ellimc3apf  15377  elply  15451  sincosq1sgn  15543  sincosq2sgn  15544  cos11  15570  logrpap0b  15593  lgsdir2lem4  15753  gausslemma2dlem0i  15779  lgsquadlem2  15800  m1lgs  15807  2lgsoddprmlem3  15833  2sqlem6  15842  2sqlem9  15846  2sqlem10  15847  vtxdfifiun  16108  wlkl1loop  16169  wlkv0  16180  wlklenvclwlk  16184  upgr2wlkdc  16186  isclwwlk  16203  isclwwlkng  16215  isclwwlknx  16225  clwwlkn2  16230  2omap  16544  pw1map  16546  subctctexmid  16551  iooref1o  16588  iswomni0  16605