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  7573  2omotaplemap  7576  ltexpi  7657  ordpipqqs  7694  ltexnqq  7728  enq0enq  7751  enq0sym  7752  enq0tr  7754  nqnq0pi  7758  genipv  7829  genprndl  7841  genprndu  7842  genpdisj  7843  genpassl  7844  genpassu  7845  addcomprg  7898  mulcomprg  7900  ltnqpr  7913  ltnqpri  7914  ltexprlemm  7920  ltexprlemdisj  7926  suplocexprlemmu  8038  suplocexprlemdisj  8040  ltsrprg  8067  mulgt0sr  8098  elreal2  8150  ltresr  8159  ltresr2  8160  axprecex  8200  axpre-ltadd  8206  axpre-mulgt0  8207  axpre-mulext  8208  axpre-suploclemres  8221  subcan2  8503  negcon1  8530  negcon2  8531  lt0neg1  8747  lt0neg2  8748  le0neg1  8749  le0neg2  8750  reapirr  8856  reapmul1  8874  reapneg  8876  remulext1  8878  apti  8901  negap0  8909  divmulap2  8955  reclt1  9175  recgt1  9176  suprleubex  9233  addltmul  9480  elznn0  9597  zapne  9657  zltlen  9662  nn0lt10b  9664  nn0lt2  9665  eluz1  9863  raluz  9916  rexuz  9918  qltlen  9978  cnref1o  9989  rpnegap  10025  ltxr  10114  xlt0neg1  10177  xlt0neg2  10178  xle0neg1  10179  xle0neg2  10180  elixx1  10236  elixx3g  10240  elioo2  10260  icc0r  10265  elicc4  10279  elioopnf  10306  elioomnf  10307  iooneg  10327  iccneg  10328  iccshftr  10333  iccshftl  10335  iccdil  10337  icccntr  10339  iccf1o  10344  elfz1  10353  0fz1  10385  fzpr  10418  fzdifsuc  10422  uzsplit  10433  elfzm1b  10439  elfzp12  10440  fznn0  10454  exfzdc  10593  zsupcllemstep  10596  flqeqceilz  10687  zmodid2  10721  expap0  10938  qsqeqor  11019  bernneq  11030  hasheqf1o  11156  ssenneg  11212  hashfibclem  11214  hashfacen  11216  ccatrn  11305  pfxsuffeqwrdeq  11398  wrd2ind  11423  sqrtmsq2i  11828  maxclpr  11915  minmax  11923  xrmaxlesup  11952  xrnegiso  11955  xrnegcon1d  11957  xrminmax  11958  clim0  11978  climrecvg1n  12041  summodc  12077  fsumsplit  12101  mertenslem2  12230  prodmodc  12272  fprodsplitdc  12290  fprod2dlemstep  12316  dvdsval2  12484  odd2np1lem  12566  even2n  12568  divalgb  12619  divalgmod  12621  bitsval  12637  bitsmod  12650  gcddvds  12667  bezoutlemmain  12702  nnwofdc  12742  isprm3  12823  prmind2  12825  dvdsprime  12827  coprm  12849  prmdvdsexp  12853  sqrt2irr  12867  sqpweven  12880  2sqpwodd  12881  pythagtriplem2  12972  pythagtrip  12989  pceu  13001  pc11  13037  ballotfilemfc0  13157  ballotfilemfcc  13158  ballotfilemodife  13162  elrest  13480  grpsubeq0  13820  grpsubadd  13822  issubg3  13930  isnsg  13940  eqger  13962  eqglact  13963  eqgid  13964  srgfcl  14138  dvdsrtr  14268  dvdsr02  14272  isunitd  14273  isrhm  14325  isrim0  14328  subsubrng2  14383  subsubrg2  14414  issubrg3  14415  opprdomnbg  14443  2idlelb  14702  mplelbascoe  14896  istopon  14927  isbasis2g  14959  isbasis3g  14960  tgss2  14993  bastop1  14997  iscld  15017  ntreq0  15046  restsn  15094  restopn2  15097  lmbr  15127  cnptoprest2  15154  txbas  15172  eltx  15173  txlm  15193  ishmeo  15218  hmeoimaf1o  15228  ispsmet  15237  ismet  15258  isxmet  15259  ismet2  15268  metn0  15292  elblps  15304  elbl  15305  bdbl  15417  qtopbasss  15435  elcncf  15487  ellimc3apf  15574  elply  15648  sincosq1sgn  15740  sincosq2sgn  15741  cos11  15767  logrpap0b  15790  lgsdir2lem4  15953  gausslemma2dlem0i  15979  lgsquadlem2  16000  m1lgs  16007  2lgsoddprmlem3  16033  2sqlem6  16042  2sqlem9  16046  2sqlem10  16047  vtxdfifiun  16341  wlkl1loop  16402  wlkv0  16413  wlklenvclwlk  16417  upgr2wlkdc  16421  isclwwlk  16438  isclwwlkng  16450  isclwwlknx  16460  clwwlkn2  16465  eupth2lem2dc  16503  eupth2lem3lem6fi  16515  pw1map  16818  subctctexmid  16823  iooref1o  16867  iswomni0  16885