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  2983  rexab2  2985  euxfr2dc  3004  reu7  3014  reu8  3015  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  ralss  3306  rexss  3307  elif  3636  prssg  3853  2ralunsn  3905  eluniab  3928  elintab  3962  dfiun2g  4025  dfiin2g  4026  cbvopab1  4185  cbvmpt  4207  axsep2  4231  bnd2  4288  opeqsn  4371  reusv3  4583  tfisi  4711  opeliunxp  4807  eliunxp  4896  relop  4907  eldm2g  4954  reldm0  4976  relrn0  5021  restidsing  5096  xpmlem  5185  elxp5  5253  cnvpom  5307  cbviota  5319  iota1  5329  sniota  5345  fncnv  5424  fnres  5477  brprcneu  5665  fnopfvb  5718  fvelrnb  5726  fvelimab  5735  fvopab3g  5752  eqfnfv3  5779  eqfnfv2f  5781  fvreseq  5783  fnreseql  5790  respreima  5807  rexrn  5816  ralrn  5817  f1ompt  5830  fsn  5851  fconstfvm  5904  fconst3m  5905  fconst4m  5906  foima2  5926  rexima  5929  ralima  5930  dff13  5943  foeqcnvco  5965  fliftfun  5971  isocnv  5986  isoini  5993  f1oiso  6001  cbvriota  6017  riotaeqimp  6030  eusvobj2  6038  oprabid  6084  eloprabga  6142  resoprab  6151  eqfnov  6162  eqfnov2  6163  ov6g  6194  funimassov  6206  ovelimab  6207  caovord2  6229  uchoice  6333  releldm2  6381  dfoprab4  6388  xporderlem  6429  poxp  6430  f1od2  6433  elsuppfng  6444  elsuppfn  6445  rexsupp  6455  mpoxopovel  6474  brtpos2  6484  brtpos0  6485  rntpos  6490  dftpos3  6495  tpostpos  6497  tpossym  6509  tposoprab  6513  tfrcllemres  6595  frecabcl  6632  frecsuclem  6639  erth2  6816  qliftfun  6853  erovlem  6863  ecopovsym  6867  ecopovsymg  6870  th3qlem1  6873  mapdm0  6899  elpmg  6900  elpm2g  6901  map0e  6922  dom2lem  7013  mapsnend  7054  mapsnen  7055  xpdom2  7084  xpf1o  7099  mapen  7101  ssfilem  7132  ssfilemd  7134  diffitest  7146  ac6sfi  7157  eqsndc  7165  ss1o0el1o  7175  2omap  7271  isoti  7300  cnvti  7312  omp1eomlem  7387  ismkvnex  7448  nninfwlporlemd  7465  en2prde  7492  netap  7570  2omotaplemap  7573  ltexpi  7654  ordpipqqs  7691  ltexnqq  7725  enq0enq  7748  enq0sym  7749  enq0tr  7751  nqnq0pi  7755  genipv  7826  genprndl  7838  genprndu  7839  genpdisj  7840  genpassl  7841  genpassu  7842  addcomprg  7895  mulcomprg  7897  ltnqpr  7910  ltnqpri  7911  ltexprlemm  7917  ltexprlemdisj  7923  suplocexprlemmu  8035  suplocexprlemdisj  8037  ltsrprg  8064  mulgt0sr  8095  elreal2  8147  ltresr  8156  ltresr2  8157  axprecex  8197  axpre-ltadd  8203  axpre-mulgt0  8204  axpre-mulext  8205  axpre-suploclemres  8218  subcan2  8500  negcon1  8527  negcon2  8528  lt0neg1  8744  lt0neg2  8745  le0neg1  8746  le0neg2  8747  reapirr  8853  reapmul1  8871  reapneg  8873  remulext1  8875  apti  8898  negap0  8906  divmulap2  8952  reclt1  9172  recgt1  9173  suprleubex  9230  addltmul  9477  elznn0  9594  zapne  9654  zltlen  9659  nn0lt10b  9661  nn0lt2  9662  eluz1  9860  raluz  9913  rexuz  9915  qltlen  9975  cnref1o  9986  rpnegap  10022  ltxr  10111  xlt0neg1  10174  xlt0neg2  10175  xle0neg1  10176  xle0neg2  10177  elixx1  10233  elixx3g  10237  elioo2  10257  icc0r  10262  elicc4  10276  elioopnf  10303  elioomnf  10304  iooneg  10324  iccneg  10325  iccshftr  10330  iccshftl  10332  iccdil  10334  icccntr  10336  iccf1o  10341  elfz1  10350  0fz1  10382  fzpr  10415  fzdifsuc  10419  uzsplit  10430  elfzm1b  10436  elfzp12  10437  fznn0  10451  exfzdc  10590  zsupcllemstep  10593  flqeqceilz  10684  zmodid2  10718  expap0  10935  qsqeqor  11016  bernneq  11026  hasheqf1o  11152  ssenneg  11208  hashfibclem  11210  hashfacen  11212  ccatrn  11301  pfxsuffeqwrdeq  11394  wrd2ind  11419  sqrtmsq2i  11824  maxclpr  11911  minmax  11919  xrmaxlesup  11948  xrnegiso  11951  xrnegcon1d  11953  xrminmax  11954  clim0  11974  climrecvg1n  12037  summodc  12073  fsumsplit  12097  mertenslem2  12226  prodmodc  12268  fprodsplitdc  12286  fprod2dlemstep  12312  dvdsval2  12480  odd2np1lem  12562  even2n  12564  divalgb  12615  divalgmod  12617  bitsval  12633  bitsmod  12646  gcddvds  12663  bezoutlemmain  12698  nnwofdc  12738  isprm3  12819  prmind2  12821  dvdsprime  12823  coprm  12845  prmdvdsexp  12849  sqrt2irr  12863  sqpweven  12876  2sqpwodd  12877  pythagtriplem2  12968  pythagtrip  12985  pceu  12997  pc11  13033  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemodife  13158  elrest  13476  grpsubeq0  13816  grpsubadd  13818  issubg3  13926  isnsg  13936  eqger  13958  eqglact  13959  eqgid  13960  srgfcl  14134  dvdsrtr  14263  dvdsr02  14267  isunitd  14268  isrhm  14320  isrim0  14323  subsubrng2  14377  subsubrg2  14408  issubrg3  14409  opprdomnbg  14437  2idlelb  14670  mplelbascoe  14864  istopon  14895  isbasis2g  14927  isbasis3g  14928  tgss2  14961  bastop1  14965  iscld  14985  ntreq0  15014  restsn  15062  restopn2  15065  lmbr  15095  cnptoprest2  15122  txbas  15140  eltx  15141  txlm  15161  ishmeo  15186  hmeoimaf1o  15196  ispsmet  15205  ismet  15226  isxmet  15227  ismet2  15236  metn0  15260  elblps  15272  elbl  15273  bdbl  15385  qtopbasss  15403  elcncf  15455  ellimc3apf  15542  elply  15616  sincosq1sgn  15708  sincosq2sgn  15709  cos11  15735  logrpap0b  15758  lgsdir2lem4  15921  gausslemma2dlem0i  15947  lgsquadlem2  15968  m1lgs  15975  2lgsoddprmlem3  16001  2sqlem6  16010  2sqlem9  16014  2sqlem10  16015  vtxdfifiun  16309  wlkl1loop  16370  wlkv0  16381  wlklenvclwlk  16385  upgr2wlkdc  16389  isclwwlk  16406  isclwwlkng  16418  isclwwlknx  16428  clwwlkn2  16433  eupth2lem2dc  16471  eupth2lem3lem6fi  16483  pw1map  16786  subctctexmid  16791  iooref1o  16835  iswomni0  16853