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  909  dn1dc  966  bilukdc  1438  nf4dc  1716  sbal1  2053  abbi  2343  necon3abid  2439  necon3bid  2441  necon1abiidc  2460  r19.21t  2605  ceqsralt  2827  ceqsrexv  2933  ceqsrex2v  2935  elab2g  2950  elrabf  2957  eueq2dc  2976  euxfrdc  2989  eqreu  2995  reu8  2999  ru  3027  sbcralt  3105  sbcrext  3106  sbcne12g  3142  csbnestgf  3177  dfss4st  3437  rexsng  3707  ralprg  3717  rexprg  3718  difsn  3805  opthpr  3850  ralunsn  3876  dfiin2g  3998  iunxsng  4041  iunxsngf  4043  elpwuni  4055  pwnss  4243  exmid01  4282  opelopabt  4350  opelopabga  4351  brabga  4352  opelopabgf  4358  elsucg  4495  elsuc2g  4496  brab2a  4772  opeliunxp  4774  posng  4791  brab2ga  4794  csbdmg  4917  elrnmpt1  4975  elrnmptg  4976  eliniseg2  5108  poleloe  5128  elxp4  5216  elxp5  5217  cnvpom  5271  sbcfung  5342  dffun8  5346  fncnv  5387  fununi  5389  fnssresb  5435  fnimaeq0  5445  funcocnv2  5599  dffn5im  5681  funimass4  5686  fnsnfv  5695  dmfco  5704  fndmdif  5742  fndmin  5744  unpreima  5762  respreima  5765  fsn2  5811  fnressn  5829  fressnfv  5830  elunirn  5896  dff13  5898  fliftel  5923  isoini  5948  f1oiso  5956  riotaeqimp  5985  acexmid  6006  fnbrovb  6052  eloprabga  6097  resoprab2  6107  ralrnmpo  6125  rexrnmpo  6126  ovid  6127  ov  6130  ovg  6150  ofrfval2  6241  fmpox  6352  1stconst  6373  2ndconst  6374  f1od2  6387  rbropapd  6394  brtpos2  6403  dfsmo2  6439  frecabcl  6551  brdifun  6715  eqerlem  6719  brecop  6780  erovlem  6782  mapsn  6845  mptelixpg  6889  map1  6973  xpsnen  6988  xpdom2  6998  xpf1o  7013  supubti  7174  infglbti  7200  ctssdccl  7286  nninfwlpoim  7354  nninfinfwlpo  7355  netap  7448  2omotaplemap  7451  ltpiord  7514  nlt1pig  7536  elinp  7669  ltdfpr  7701  genpassl  7719  genpassu  7720  1idprl  7785  1idpru  7786  gt0srpr  7943  mappsrprg  7999  map2psrprg  8000  peano2nnnn  8048  recidpirq  8053  axprecex  8075  xrlenlt  8219  addsubeq4  8369  renegcl  8415  lesub0  8634  recexaplem2  8807  conjmulap  8884  rerecclap  8885  creui  9115  peano2nn  9130  nndiv  9159  elznn0  9469  eqreznegel  9817  negelrp  9891  ltxr  9979  divelunit  10206  iccf1o  10208  elfz2  10219  elfzp1  10276  fzdifsuc  10285  fznn  10293  nelfzo  10356  fzosplitsni  10449  fvinim0ffz  10455  infssuzex  10461  zsupssdc  10466  frec2uzisod  10637  sq11i  10859  wrdval  11082  csbwrdg  11109  swrdnd  11199  wrd2ind  11263  cjreb  11385  rexfiuz  11508  cau3lem  11633  pwm1geoserap1  12027  mertensabs  12056  divides  12308  dvdsabseq  12366  odd2np1  12392  oddm1even  12394  modremain  12448  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlemmain  12527  bezoutlema  12528  bezoutlemb  12529  isprm2  12647  isprm4  12649  dvdsnprmd  12655  oddprmdvds  12885  4sqlem2  12920  4sqlem12  12933  xpsfrnel2  13387  issubm  13513  grplmulf1o  13615  grplactcnv  13643  issubg  13718  elnmz  13753  isghm  13788  ghmeqker  13816  srg1zr  13958  iscrng2  13986  issubrng  14171  aprval  14254  zndvds  14621  znleval  14625  psrbag  14641  istopg  14681  basgen2  14763  isnei  14826  restdis  14866  iscn  14879  iscnp  14881  lmbr2  14896  lmbrf  14897  txcn  14957  cnmpt21  14973  blres  15116  isxms2  15134  metrest  15188  metcnp  15194  txmetcnp  15200  txmetcn  15201  cnblcld  15217  reopnap  15228  ioocosf1o  15536  mpodvdsmulf1o  15672  gausslemma2dlem0i  15744  gausslemma2dlem1a  15745  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  2lgslem1a  15775  isuhgrm  15879  isushgrm  15880  isupgren  15903  isumgren  15913  isuspgren  15963  isusgren  15964  iswlk  16044  wlk1walkdom  16080  istrl  16104  bj-nn0sucALT  16365  apdiff  16446