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  912  dn1dc  969  bilukdc  1441  nf4dc  1718  sbal1  2058  abbibcom  2348  abbib  2352  necon3abid  2453  necon3bid  2455  necon1abiidc  2474  r19.21t  2619  ceqsralt  2843  ceqsrexv  2950  ceqsrex2v  2952  elab2g  2967  elrabf  2974  eueq2dc  2993  euxfrdc  3006  eqreu  3012  reu8  3016  ru  3044  sbcralt  3122  sbcrext  3123  sbcne12g  3159  csbnestgf  3194  dfss4st  3458  rexsng  3735  ralprg  3745  rexprg  3746  difsn  3836  opthpr  3881  ralunsn  3907  dfiin2g  4029  iunxsng  4072  iunxsngf  4074  elpwuni  4086  pwnss  4277  exmid01  4316  opelopabt  4385  opelopabga  4386  brabga  4387  opelopabgf  4393  elsucg  4530  elsuc2g  4531  brab2a  4808  opeliunxp  4810  posng  4827  brab2ga  4830  csbdmg  4955  elrnmpt1  5013  elrnmptg  5014  eliniseg2  5147  poleloe  5167  elxp4  5255  elxp5  5256  cnvpom  5310  sbcfung  5381  dffun8  5385  fncnv  5427  fununi  5429  fnssresb  5475  fnimaeq0  5485  funcocnv2  5644  dffn5im  5727  funimass4  5732  fnsnfv  5741  dmfco  5750  fndmdif  5788  fndmin  5790  unpreima  5807  respreima  5810  fsn2  5856  fnressn  5875  fressnfv  5876  elunirn  5945  dff13  5947  fliftel  5972  isoini  5997  f1oiso  6005  riotaeqimp  6036  acexmid  6057  fnbrovb  6103  eloprabga  6148  resoprab2  6158  ralrnmpo  6176  rexrnmpo  6177  ovid  6178  ov  6181  ovg  6201  ofrfval2  6292  fmpox  6409  1stconst  6430  2ndconst  6431  f1od2  6444  rbropapd  6486  brtpos2  6495  dfsmo2  6531  frecabcl  6643  brdifun  6807  eqerlem  6811  brecop  6872  erovlem  6874  mapsnd  6936  mapsn  6938  mptelixpg  6982  map1  7067  xpsnen  7085  xpdom2  7095  xpf1o  7110  mapunen  7117  supubti  7303  infglbti  7329  ctssdccl  7415  nninfwlpoim  7483  nninfinfwlpo  7484  netap  7584  2omotaplemap  7587  ltpiord  7650  nlt1pig  7672  elinp  7805  ltdfpr  7837  genpassl  7855  genpassu  7856  1idprl  7921  1idpru  7922  gt0srpr  8079  mappsrprg  8135  map2psrprg  8136  peano2nnnn  8184  recidpirq  8189  axprecex  8211  xrlenlt  8354  addsubeq4  8505  renegcl  8551  lesub0  8771  recexaplem2  8944  conjmulap  9023  rerecclap  9024  creui  9254  peano2nn  9269  nndiv  9298  elznn0  9612  eqreznegel  9967  negelrp  10041  ltxr  10130  divelunit  10357  iccf1o  10360  elfz2  10371  elfzp1  10431  fzdifsuc  10440  fznn  10448  nelfzo  10511  fzosplitsni  10606  fvinim0ffz  10612  infssuzex  10618  zsupssdc  10625  frec2uzisod  10796  sq11i  11018  wrdval  11255  csbwrdg  11282  swrdnd  11379  wrd2ind  11443  cjreb  11579  rexfiuz  11702  cau3lem  11827  pwm1geoserap1  12222  mertensabs  12251  divides  12503  dvdsabseq  12561  odd2np1  12587  oddm1even  12589  modremain  12643  bezoutlemnewy  12720  bezoutlemstep  12721  bezoutlemmain  12722  bezoutlema  12723  bezoutlemb  12724  isprm2  12842  isprm4  12844  dvdsnprmd  12850  oddprmdvds  13080  4sqlem2  13115  4sqlem12  13128  xpsfrnel2  13613  issubm  13730  grplmulf1o  13832  grplactcnv  13860  issubg  13929  elnmz  13964  isghm  13999  ghmeqker  14027  rng1zrlem  14201  iscrng2  14261  issubrng  14448  aprval  14532  zndvds  14926  znleval  14930  psrbag  14946  istopg  14993  basgen2  15075  isnei  15138  restdis  15178  iscn  15191  iscnp  15193  lmbr2  15208  lmbrf  15209  txcn  15269  cnmpt21  15285  blres  15428  isxms2  15446  metrest  15500  metcnp  15506  txmetcnp  15512  txmetcn  15513  cnblcld  15529  reopnap  15540  ioocosf1o  15848  mpodvdsmulf1o  15987  gausslemma2dlem0i  16059  gausslemma2dlem1a  16060  lgseisenlem2  16073  lgsquadlem1  16079  lgsquadlem2  16080  2lgslem1a  16090  isuhgrm  16195  isushgrm  16196  isupgren  16219  isumgren  16229  isuspgren  16281  isusgren  16282  uhgr0v0e  16358  vtxdg0v  16418  iswlk  16447  wlk1walkdom  16483  istrl  16509  clwwlkn1  16542  clwwlkn2  16545  clwwlknonel  16556  clwwlknun  16565  iseupth  16571  eupthres  16581  eupth2lem1  16582  eupth2lemsfi  16602  bj-nn0sucALT  16887  apdiff  16971