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  896  pm5.75  971  xordidc  1444  19.17  1605  alexdc  1668  nf4dc  1718  abeq2d  2347  eqabrd  2372  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvrab  2813  ceqsralt  2843  ralab2  2984  rexab2  2986  euxfr2dc  3005  reu7  3015  reu8  3016  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  ralss  3308  rexss  3309  elif  3638  prssg  3856  2ralunsn  3908  eluniab  3931  elintab  3965  dfiun2g  4028  dfiin2g  4029  cbvopab1  4188  cbvmpt  4210  axsep2  4234  bnd2  4291  opeqsn  4374  reusv3  4586  tfisi  4714  opeliunxp  4810  eliunxp  4899  relop  4910  eldm2g  4957  reldm0  4979  relrn0  5024  restidsing  5099  xpmlem  5188  elxp5  5256  cnvpom  5310  cbviota  5322  iota1  5332  sniota  5348  fncnv  5427  fnres  5480  brprcneu  5668  fnopfvb  5721  fvelrnb  5729  fvelimab  5738  fvopab3g  5755  eqfnfv3  5782  eqfnfv2f  5784  fvreseq  5786  fnreseql  5793  respreima  5810  rexrn  5819  ralrn  5820  f1ompt  5833  fsn  5854  fconstfvm  5907  fconst3m  5908  fconst4m  5909  foima2  5930  rexima  5933  ralima  5934  dff13  5947  foeqcnvco  5969  fliftfun  5975  isocnv  5990  isoini  5997  f1oiso  6005  cbvriota  6023  riotaeqimp  6036  eusvobj2  6044  oprabid  6090  eloprabga  6148  resoprab  6157  eqfnov  6168  eqfnov2  6169  ov6g  6200  funimassov  6212  ovelimab  6213  caovord2  6235  uchoice  6344  releldm2  6392  dfoprab4  6399  xporderlem  6440  poxp  6441  f1od2  6444  elsuppfng  6455  elsuppfn  6456  rexsupp  6466  mpoxopovel  6485  brtpos2  6495  brtpos0  6496  rntpos  6501  dftpos3  6506  tpostpos  6508  tpossym  6520  tposoprab  6524  tfrcllemres  6606  frecabcl  6643  frecsuclem  6650  erth2  6827  qliftfun  6864  erovlem  6874  ecopovsym  6878  ecopovsymg  6881  th3qlem1  6884  mapdm0  6910  elpmg  6911  elpm2g  6912  map0e  6933  dom2lem  7024  mapsnend  7065  mapsnen  7066  xpdom2  7095  xpf1o  7110  mapen  7112  ssfilem  7143  ssfilemd  7145  diffitest  7157  ac6sfi  7168  eqsndc  7176  ss1o0el1o  7186  2omap  7282  isoti  7311  cnvti  7323  omp1eomlem  7398  ismkvnex  7459  nninfwlporlemd  7476  en2prde  7503  netap  7584  2omotaplemap  7587  ltexpi  7668  ordpipqqs  7705  ltexnqq  7739  enq0enq  7762  enq0sym  7763  enq0tr  7765  nqnq0pi  7769  genipv  7840  genprndl  7852  genprndu  7853  genpdisj  7854  genpassl  7855  genpassu  7856  addcomprg  7909  mulcomprg  7911  ltnqpr  7924  ltnqpri  7925  ltexprlemm  7931  ltexprlemdisj  7937  suplocexprlemmu  8049  suplocexprlemdisj  8051  ltsrprg  8078  mulgt0sr  8109  elreal2  8161  ltresr  8170  ltresr2  8171  axprecex  8211  axpre-ltadd  8217  axpre-mulgt0  8218  axpre-mulext  8219  axpre-suploclemres  8232  subcan2  8515  negcon1  8542  negcon2  8543  lt0neg1  8760  lt0neg2  8761  le0neg1  8762  le0neg2  8763  reapirr  8869  reapmul1  8887  reapneg  8889  remulext1  8891  apti  8914  negap0  8922  divmulap2  8970  reclt1  9190  recgt1  9191  suprleubex  9248  addltmul  9495  elznn0  9612  zapne  9672  zltlen  9677  nn0lt10b  9679  nn0lt2  9680  eluz1  9878  raluz  9931  rexuz  9933  qltlen  9993  cnref1o  10004  rpnegap  10040  ltxr  10130  xlt0neg1  10193  xlt0neg2  10194  xle0neg1  10195  xle0neg2  10196  elixx1  10252  elixx3g  10256  elioo2  10276  icc0r  10281  elicc4  10295  elioopnf  10322  elioomnf  10323  iooneg  10343  iccneg  10344  iccshftr  10349  iccshftl  10351  iccdil  10353  icccntr  10355  iccf1o  10360  elfz1  10369  0fz1  10402  fzpr  10436  fzdifsuc  10440  uzsplit  10451  elfzm1b  10457  elfzp12  10458  fznn0  10472  exfzdc  10611  zsupcllemstep  10614  flqeqceilz  10707  zmodid2  10741  expap0  10958  qsqeqor  11039  bernneq  11050  hasheqf1o  11176  ssenneg  11232  hashfibclem  11234  hashfacen  11236  ccatrn  11325  pfxsuffeqwrdeq  11418  wrd2ind  11443  sqrtmsq2i  11848  maxclpr  11935  minmax  11943  xrmaxlesup  11972  xrnegiso  11975  xrnegcon1d  11977  xrminmax  11978  clim0  11998  climrecvg1n  12061  summodc  12097  fsumsplit  12121  mertenslem2  12250  prodmodc  12292  fprodsplitdc  12310  fprod2dlemstep  12336  dvdsval2  12504  odd2np1lem  12586  even2n  12588  divalgb  12639  divalgmod  12641  bitsval  12657  bitsmod  12670  gcddvds  12687  bezoutlemmain  12722  nnwofdc  12762  isprm3  12843  prmind2  12845  dvdsprime  12847  coprm  12869  prmdvdsexp  12873  sqrt2irr  12887  sqpweven  12900  2sqpwodd  12901  pythagtriplem2  12992  pythagtrip  13009  pceu  13021  pc11  13057  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemodife  13187  elrest  13546  grpsubeq0  13844  grpsubadd  13846  issubg3  13948  isnsg  13958  eqger  13980  eqglact  13981  eqgid  13982  srgfcl  14219  dvdsrtr  14349  dvdsr02  14353  isunitd  14354  isrhm  14406  isrim0  14409  subsubrng2  14464  subsubrg2  14495  issubrg3  14496  opprdomnbg  14524  2idlelb  14782  mplelbascoe  14976  istopon  15007  isbasis2g  15039  isbasis3g  15040  tgss2  15073  bastop1  15077  iscld  15097  ntreq0  15126  restsn  15174  restopn2  15177  lmbr  15207  cnptoprest2  15234  txbas  15252  eltx  15253  txlm  15273  ishmeo  15298  hmeoimaf1o  15308  ispsmet  15317  ismet  15338  isxmet  15339  ismet2  15348  metn0  15372  elblps  15384  elbl  15385  bdbl  15497  qtopbasss  15515  elcncf  15567  ellimc3apf  15654  elply  15728  sincosq1sgn  15820  sincosq2sgn  15821  cos11  15847  logrpap0b  15870  lgsdir2lem4  16033  gausslemma2dlem0i  16059  lgsquadlem2  16080  m1lgs  16087  2lgsoddprmlem3  16113  2sqlem6  16122  2sqlem9  16126  2sqlem10  16127  vtxdfifiun  16421  wlkl1loop  16482  wlkv0  16493  wlklenvclwlk  16497  upgr2wlkdc  16501  isclwwlk  16518  isclwwlkng  16530  isclwwlknx  16540  clwwlkn2  16545  eupth2lem2dc  16583  eupth2lem3lem6fi  16595  pw1map  16908  subctctexmid  16913  iooref1o  16957  iswomni0  16975