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  892  pm5.75  967  xordidc  1421  19.17  1582  alexdc  1645  nf4dc  1696  abeq2d  2322  cbvralf  2736  cbvrexf  2737  cbvreu  2743  cbvrab  2777  ceqsralt  2807  ralab2  2947  rexab2  2949  euxfr2dc  2968  reu7  2978  reu8  2979  cbvralcsf  3167  cbvrexcsf  3168  cbvreucsf  3169  cbvrabcsf  3170  ralss  3270  rexss  3271  elif  3594  prssg  3804  2ralunsn  3856  eluniab  3879  elintab  3913  dfiun2g  3976  dfiin2g  3977  cbvopab1  4136  cbvmpt  4158  axsep2  4182  bnd2  4236  opeqsn  4318  reusv3  4528  tfisi  4656  opeliunxp  4751  eliunxp  4838  relop  4849  eldm2g  4896  reldm0  4918  relrn0  4962  restidsing  5037  xpmlem  5125  elxp5  5193  cnvpom  5247  cbviota  5259  iota1  5269  sniota  5285  fncnv  5363  fnres  5416  brprcneu  5596  fnopfvb  5647  fvelrnb  5654  fvelimab  5663  fvopab3g  5680  eqfnfv3  5707  eqfnfv2f  5709  fvreseq  5711  fnreseql  5718  rexsupp  5732  respreima  5736  rexrn  5745  ralrn  5746  f1ompt  5759  fsn  5780  fconstfvm  5830  fconst3m  5831  fconst4m  5832  foima2  5848  rexima  5851  ralima  5852  dff13  5865  foeqcnvco  5887  fliftfun  5893  isocnv  5908  isoini  5915  f1oiso  5923  cbvriota  5939  riotaeqimp  5952  eusvobj2  5960  oprabid  6006  eloprabga  6062  resoprab  6071  eqfnov  6082  eqfnov2  6083  ov6g  6114  funimassov  6126  ovelimab  6127  caovord2  6149  uchoice  6253  releldm2  6301  dfoprab4  6308  xporderlem  6347  poxp  6348  f1od2  6351  mpoxopovel  6357  brtpos2  6367  brtpos0  6368  rntpos  6373  dftpos3  6378  tpostpos  6380  tpossym  6392  tposoprab  6396  tfrcllemres  6478  frecabcl  6515  frecsuclem  6522  erth2  6697  qliftfun  6734  erovlem  6744  ecopovsym  6748  ecopovsymg  6751  th3qlem1  6754  mapdm0  6780  elpmg  6781  elpm2g  6782  map0e  6803  dom2lem  6893  mapsnen  6934  xpdom2  6958  xpf1o  6973  mapen  6975  ssfilem  7005  diffitest  7017  ac6sfi  7028  ss1o0el1o  7043  isoti  7142  cnvti  7154  omp1eomlem  7229  ismkvnex  7290  nninfwlporlemd  7307  en2prde  7334  netap  7408  2omotaplemap  7411  ltexpi  7492  ordpipqqs  7529  ltexnqq  7563  enq0enq  7586  enq0sym  7587  enq0tr  7589  nqnq0pi  7593  genipv  7664  genprndl  7676  genprndu  7677  genpdisj  7678  genpassl  7679  genpassu  7680  addcomprg  7733  mulcomprg  7735  ltnqpr  7748  ltnqpri  7749  ltexprlemm  7755  ltexprlemdisj  7761  suplocexprlemmu  7873  suplocexprlemdisj  7875  ltsrprg  7902  mulgt0sr  7933  elreal2  7985  ltresr  7994  ltresr2  7995  axprecex  8035  axpre-ltadd  8041  axpre-mulgt0  8042  axpre-mulext  8043  axpre-suploclemres  8056  subcan2  8339  negcon1  8366  negcon2  8367  lt0neg1  8583  lt0neg2  8584  le0neg1  8585  le0neg2  8586  reapirr  8692  reapmul1  8710  reapneg  8712  remulext1  8714  apti  8737  negap0  8745  divmulap2  8791  reclt1  9011  recgt1  9012  suprleubex  9069  addltmul  9316  elznn0  9429  zapne  9489  zltlen  9493  nn0lt10b  9495  nn0lt2  9496  eluz1  9694  raluz  9741  rexuz  9743  qltlen  9803  cnref1o  9814  rpnegap  9850  ltxr  9939  xlt0neg1  10002  xlt0neg2  10003  xle0neg1  10004  xle0neg2  10005  elixx1  10061  elixx3g  10065  elioo2  10085  icc0r  10090  elicc4  10104  elioopnf  10131  elioomnf  10132  iooneg  10152  iccneg  10153  iccshftr  10158  iccshftl  10160  iccdil  10162  icccntr  10164  iccf1o  10168  elfz1  10177  0fz1  10209  fzpr  10241  fzdifsuc  10245  uzsplit  10256  elfzm1b  10262  elfzp12  10263  fznn0  10277  exfzdc  10413  zsupcllemstep  10416  flqeqceilz  10507  zmodid2  10541  expap0  10758  qsqeqor  10839  bernneq  10849  hasheqf1o  10974  hashfacen  11025  ccatrn  11110  pfxsuffeqwrdeq  11196  wrd2ind  11221  sqrtmsq2i  11612  maxclpr  11699  minmax  11707  xrmaxlesup  11736  xrnegiso  11739  xrnegcon1d  11741  xrminmax  11742  clim0  11762  climrecvg1n  11825  summodc  11860  fsumsplit  11884  mertenslem2  12013  prodmodc  12055  fprodsplitdc  12073  fprod2dlemstep  12099  dvdsval2  12267  odd2np1lem  12349  even2n  12351  divalgb  12402  divalgmod  12404  bitsval  12420  bitsmod  12433  gcddvds  12450  bezoutlemmain  12485  nnwofdc  12525  isprm3  12606  prmind2  12608  dvdsprime  12610  coprm  12632  prmdvdsexp  12636  sqrt2irr  12650  sqpweven  12663  2sqpwodd  12664  pythagtriplem2  12755  pythagtrip  12772  pceu  12784  pc11  12820  elrest  13245  grpsubeq0  13585  grpsubadd  13587  issubg3  13695  isnsg  13705  eqger  13727  eqglact  13728  eqgid  13729  srgfcl  13902  dvdsrtr  14030  dvdsr02  14034  isunitd  14035  isrhm  14087  isrim0  14090  subsubrng2  14144  subsubrg2  14175  issubrg3  14176  opprdomnbg  14203  2idlelb  14434  mplelbascoe  14621  istopon  14652  isbasis2g  14684  isbasis3g  14685  tgss2  14718  bastop1  14722  iscld  14742  ntreq0  14771  restsn  14819  restopn2  14822  lmbr  14852  cnptoprest2  14879  txbas  14897  eltx  14898  txlm  14918  ishmeo  14943  hmeoimaf1o  14953  ispsmet  14962  ismet  14983  isxmet  14984  ismet2  14993  metn0  15017  elblps  15029  elbl  15030  bdbl  15142  qtopbasss  15160  elcncf  15212  ellimc3apf  15299  elply  15373  sincosq1sgn  15465  sincosq2sgn  15466  cos11  15492  logrpap0b  15515  lgsdir2lem4  15675  gausslemma2dlem0i  15701  lgsquadlem2  15722  m1lgs  15729  2lgsoddprmlem3  15755  2sqlem6  15764  2sqlem9  15768  2sqlem10  15769  2omap  16270  pw1map  16272  subctctexmid  16277  iooref1o  16313  iswomni0  16330