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  906  dn1dc  963  bilukdc  1416  nf4dc  1694  sbal1  2031  abbi  2320  necon3abid  2416  necon3bid  2418  necon1abiidc  2437  r19.21t  2582  ceqsralt  2800  ceqsrexv  2904  ceqsrex2v  2906  elab2g  2921  elrabf  2928  eueq2dc  2947  euxfrdc  2960  eqreu  2966  reu8  2970  ru  2998  sbcralt  3076  sbcrext  3077  sbcne12g  3112  csbnestgf  3147  dfss4st  3407  rexsng  3675  ralprg  3685  rexprg  3686  difsn  3772  opthpr  3815  ralunsn  3840  dfiin2g  3962  iunxsng  4005  iunxsngf  4007  elpwuni  4019  pwnss  4207  exmid01  4246  opelopabt  4312  opelopabga  4313  brabga  4314  opelopabgf  4320  elsucg  4455  elsuc2g  4456  brab2a  4732  opeliunxp  4734  posng  4751  brab2ga  4754  csbdmg  4877  elrnmpt1  4934  elrnmptg  4935  eliniseg2  5067  poleloe  5087  elxp4  5175  elxp5  5176  cnvpom  5230  sbcfung  5300  dffun8  5304  fncnv  5345  fununi  5347  fnssresb  5393  fnimaeq0  5403  funcocnv2  5554  dffn5im  5631  funimass4  5636  fnsnfv  5645  dmfco  5654  fndmdif  5692  fndmin  5694  unpreima  5712  respreima  5715  fsn2  5761  fnressn  5777  fressnfv  5778  elunirn  5842  dff13  5844  fliftel  5869  isoini  5894  f1oiso  5902  acexmid  5950  eloprabga  6039  resoprab2  6049  ralrnmpo  6067  rexrnmpo  6068  ovid  6069  ov  6072  ovg  6092  ofrfval2  6182  fmpox  6293  1stconst  6314  2ndconst  6315  f1od2  6328  rbropapd  6335  brtpos2  6344  dfsmo2  6380  frecabcl  6492  brdifun  6654  eqerlem  6658  brecop  6719  erovlem  6721  mapsn  6784  mptelixpg  6828  map1  6911  xpsnen  6923  xpdom2  6933  xpf1o  6948  supubti  7108  infglbti  7134  ctssdccl  7220  nninfwlpoim  7288  nninfinfwlpo  7289  netap  7373  2omotaplemap  7376  ltpiord  7439  nlt1pig  7461  elinp  7594  ltdfpr  7626  genpassl  7644  genpassu  7645  1idprl  7710  1idpru  7711  gt0srpr  7868  mappsrprg  7924  map2psrprg  7925  peano2nnnn  7973  recidpirq  7978  axprecex  8000  xrlenlt  8144  addsubeq4  8294  renegcl  8340  lesub0  8559  recexaplem2  8732  conjmulap  8809  rerecclap  8810  creui  9040  peano2nn  9055  nndiv  9084  elznn0  9394  eqreznegel  9742  negelrp  9816  ltxr  9904  divelunit  10131  iccf1o  10133  elfz2  10144  elfzp1  10201  fzdifsuc  10210  fznn  10218  nelfzo  10281  fzosplitsni  10371  fvinim0ffz  10377  infssuzex  10383  zsupssdc  10388  frec2uzisod  10559  sq11i  10781  wrdval  11004  csbwrdg  11030  swrdnd  11120  cjreb  11221  rexfiuz  11344  cau3lem  11469  pwm1geoserap1  11863  mertensabs  11892  divides  12144  dvdsabseq  12202  odd2np1  12228  oddm1even  12230  modremain  12284  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlemmain  12363  bezoutlema  12364  bezoutlemb  12365  isprm2  12483  isprm4  12485  dvdsnprmd  12491  oddprmdvds  12721  4sqlem2  12756  4sqlem12  12769  xpsfrnel2  13222  issubm  13348  grplmulf1o  13450  grplactcnv  13478  issubg  13553  elnmz  13588  isghm  13623  ghmeqker  13651  srg1zr  13793  iscrng2  13821  issubrng  14005  aprval  14088  zndvds  14455  znleval  14459  psrbag  14475  istopg  14515  basgen2  14597  isnei  14660  restdis  14700  iscn  14713  iscnp  14715  lmbr2  14730  lmbrf  14731  txcn  14791  cnmpt21  14807  blres  14950  isxms2  14968  metrest  15022  metcnp  15028  txmetcnp  15034  txmetcn  15035  cnblcld  15051  reopnap  15062  ioocosf1o  15370  mpodvdsmulf1o  15506  gausslemma2dlem0i  15578  gausslemma2dlem1a  15579  lgseisenlem2  15592  lgsquadlem1  15598  lgsquadlem2  15599  2lgslem1a  15609  isuhgrm  15711  isushgrm  15712  bj-nn0sucALT  15988  apdiff  16061