Theorem bitrid 192

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
bitrid.1	⊢ (𝜑 ↔ 𝜓)
bitrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitrid	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem bitrid

Step	Hyp	Ref	Expression
1		bitrid.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3		bitrid.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 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:  bitr2id  193  bitr3id  194  3bitr4g  223  imim21b  253  pm5.17dc  905  dn1dc  962  bilukdc  1407  nf4dc  1684  sbal1  2021  abbi  2310  necon3abid  2406  necon3bid  2408  necon1abiidc  2427  r19.21t  2572  ceqsralt  2790  ceqsrexv  2894  ceqsrex2v  2896  elab2g  2911  elrabf  2918  eueq2dc  2937  euxfrdc  2950  eqreu  2956  reu8  2960  ru  2988  sbcralt  3066  sbcrext  3067  sbcne12g  3102  csbnestgf  3137  dfss4st  3397  rexsng  3664  ralprg  3674  rexprg  3675  difsn  3760  opthpr  3803  ralunsn  3828  dfiin2g  3950  iunxsng  3993  iunxsngf  3995  elpwuni  4007  pwnss  4193  exmid01  4232  opelopabt  4297  opelopabga  4298  brabga  4299  opelopabgf  4305  elsucg  4440  elsuc2g  4441  brab2a  4717  opeliunxp  4719  posng  4736  brab2ga  4739  csbdmg  4861  elrnmpt1  4918  elrnmptg  4919  eliniseg2  5050  poleloe  5070  elxp4  5158  elxp5  5159  cnvpom  5213  sbcfung  5283  dffun8  5287  fncnv  5325  fununi  5327  fnssresb  5373  fnimaeq0  5382  funcocnv2  5532  dffn5im  5609  funimass4  5614  fnsnfv  5623  dmfco  5632  fndmdif  5670  fndmin  5672  unpreima  5690  respreima  5693  fsn2  5739  fnressn  5751  fressnfv  5752  elunirn  5816  dff13  5818  fliftel  5843  isoini  5868  f1oiso  5876  acexmid  5924  eloprabga  6013  resoprab2  6023  ralrnmpo  6041  rexrnmpo  6042  ovid  6043  ov  6046  ovg  6066  ofrfval2  6156  fmpox  6267  1stconst  6288  2ndconst  6289  f1od2  6302  rbropapd  6309  brtpos2  6318  dfsmo2  6354  frecabcl  6466  brdifun  6628  eqerlem  6632  brecop  6693  erovlem  6695  mapsn  6758  mptelixpg  6802  map1  6880  xpsnen  6889  xpdom2  6899  xpf1o  6914  supubti  7074  infglbti  7100  ctssdccl  7186  nninfwlpoim  7253  netap  7337  2omotaplemap  7340  ltpiord  7403  nlt1pig  7425  elinp  7558  ltdfpr  7590  genpassl  7608  genpassu  7609  1idprl  7674  1idpru  7675  gt0srpr  7832  mappsrprg  7888  map2psrprg  7889  peano2nnnn  7937  recidpirq  7942  axprecex  7964  xrlenlt  8108  addsubeq4  8258  renegcl  8304  lesub0  8523  recexaplem2  8696  conjmulap  8773  rerecclap  8774  creui  9004  peano2nn  9019  nndiv  9048  elznn0  9358  eqreznegel  9705  negelrp  9779  ltxr  9867  divelunit  10094  iccf1o  10096  elfz2  10107  elfzp1  10164  fzdifsuc  10173  fznn  10181  nelfzo  10244  fzosplitsni  10328  fvinim0ffz  10334  infssuzex  10340  zsupssdc  10345  frec2uzisod  10516  sq11i  10738  wrdval  10955  csbwrdg  10981  cjreb  11048  rexfiuz  11171  cau3lem  11296  pwm1geoserap1  11690  mertensabs  11719  divides  11971  dvdsabseq  12029  odd2np1  12055  oddm1even  12057  modremain  12111  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlema  12191  bezoutlemb  12192  isprm2  12310  isprm4  12312  dvdsnprmd  12318  oddprmdvds  12548  4sqlem2  12583  4sqlem12  12596  xpsfrnel2  13048  issubm  13174  grplmulf1o  13276  grplactcnv  13304  issubg  13379  elnmz  13414  isghm  13449  ghmeqker  13477  srg1zr  13619  iscrng2  13647  issubrng  13831  aprval  13914  zndvds  14281  znleval  14285  psrbag  14299  istopg  14319  basgen2  14401  isnei  14464  restdis  14504  iscn  14517  iscnp  14519  lmbr2  14534  lmbrf  14535  txcn  14595  cnmpt21  14611  blres  14754  isxms2  14772  metrest  14826  metcnp  14832  txmetcnp  14838  txmetcn  14839  cnblcld  14855  reopnap  14866  ioocosf1o  15174  mpodvdsmulf1o  15310  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem1a  15413  bj-nn0sucALT  15708  apdiff  15779