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  7254  nninfinfwlpo  7255  netap  7339  2omotaplemap  7342  ltpiord  7405  nlt1pig  7427  elinp  7560  ltdfpr  7592  genpassl  7610  genpassu  7611  1idprl  7676  1idpru  7677  gt0srpr  7834  mappsrprg  7890  map2psrprg  7891  peano2nnnn  7939  recidpirq  7944  axprecex  7966  xrlenlt  8110  addsubeq4  8260  renegcl  8306  lesub0  8525  recexaplem2  8698  conjmulap  8775  rerecclap  8776  creui  9006  peano2nn  9021  nndiv  9050  elznn0  9360  eqreznegel  9707  negelrp  9781  ltxr  9869  divelunit  10096  iccf1o  10098  elfz2  10109  elfzp1  10166  fzdifsuc  10175  fznn  10183  nelfzo  10246  fzosplitsni  10330  fvinim0ffz  10336  infssuzex  10342  zsupssdc  10347  frec2uzisod  10518  sq11i  10740  wrdval  10957  csbwrdg  10983  cjreb  11050  rexfiuz  11173  cau3lem  11298  pwm1geoserap1  11692  mertensabs  11721  divides  11973  dvdsabseq  12031  odd2np1  12057  oddm1even  12059  modremain  12113  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlema  12193  bezoutlemb  12194  isprm2  12312  isprm4  12314  dvdsnprmd  12320  oddprmdvds  12550  4sqlem2  12585  4sqlem12  12598  xpsfrnel2  13050  issubm  13176  grplmulf1o  13278  grplactcnv  13306  issubg  13381  elnmz  13416  isghm  13451  ghmeqker  13479  srg1zr  13621  iscrng2  13649  issubrng  13833  aprval  13916  zndvds  14283  znleval  14287  psrbag  14301  istopg  14321  basgen2  14403  isnei  14466  restdis  14506  iscn  14519  iscnp  14521  lmbr2  14536  lmbrf  14537  txcn  14597  cnmpt21  14613  blres  14756  isxms2  14774  metrest  14828  metcnp  14834  txmetcnp  14840  txmetcn  14841  cnblcld  14857  reopnap  14868  ioocosf1o  15176  mpodvdsmulf1o  15312  gausslemma2dlem0i  15384  gausslemma2dlem1a  15385  lgseisenlem2  15398  lgsquadlem1  15404  lgsquadlem2  15405  2lgslem1a  15415  bj-nn0sucALT  15710  apdiff  15783