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  2056  abbibcom  2346  abbib  2350  necon3abid  2451  necon3bid  2453  necon1abiidc  2472  r19.21t  2617  ceqsralt  2840  ceqsrexv  2946  ceqsrex2v  2948  elab2g  2963  elrabf  2970  eueq2dc  2989  euxfrdc  3002  eqreu  3008  reu8  3012  ru  3040  sbcralt  3118  sbcrext  3119  sbcne12g  3155  csbnestgf  3190  dfss4st  3453  rexsng  3729  ralprg  3739  rexprg  3740  difsn  3830  opthpr  3875  ralunsn  3901  dfiin2g  4023  iunxsng  4066  iunxsngf  4068  elpwuni  4080  pwnss  4271  exmid01  4310  opelopabt  4379  opelopabga  4380  brabga  4381  opelopabgf  4387  elsucg  4524  elsuc2g  4525  brab2a  4802  opeliunxp  4804  posng  4821  brab2ga  4824  csbdmg  4949  elrnmpt1  5007  elrnmptg  5008  eliniseg2  5141  poleloe  5161  elxp4  5249  elxp5  5250  cnvpom  5304  sbcfung  5375  dffun8  5379  fncnv  5421  fununi  5423  fnssresb  5469  fnimaeq0  5479  funcocnv2  5638  dffn5im  5721  funimass4  5726  fnsnfv  5735  dmfco  5744  fndmdif  5782  fndmin  5784  unpreima  5801  respreima  5804  fsn2  5850  fnressn  5869  fressnfv  5870  elunirn  5938  dff13  5940  fliftel  5965  isoini  5990  f1oiso  5998  riotaeqimp  6027  acexmid  6048  fnbrovb  6094  eloprabga  6139  resoprab2  6149  ralrnmpo  6167  rexrnmpo  6168  ovid  6169  ov  6172  ovg  6192  ofrfval2  6282  fmpox  6395  1stconst  6416  2ndconst  6417  f1od2  6430  rbropapd  6472  brtpos2  6481  dfsmo2  6517  frecabcl  6629  brdifun  6793  eqerlem  6797  brecop  6858  erovlem  6860  mapsnd  6922  mapsn  6924  mptelixpg  6968  map1  7053  xpsnen  7071  xpdom2  7081  xpf1o  7096  mapunen  7103  supubti  7289  infglbti  7315  ctssdccl  7401  nninfwlpoim  7469  nninfinfwlpo  7470  netap  7564  2omotaplemap  7567  ltpiord  7630  nlt1pig  7652  elinp  7785  ltdfpr  7817  genpassl  7835  genpassu  7836  1idprl  7901  1idpru  7902  gt0srpr  8059  mappsrprg  8115  map2psrprg  8116  peano2nnnn  8164  recidpirq  8169  axprecex  8191  xrlenlt  8334  addsubeq4  8484  renegcl  8530  lesub0  8749  recexaplem2  8922  conjmulap  8999  rerecclap  9000  creui  9230  peano2nn  9245  nndiv  9274  elznn0  9588  eqreznegel  9942  negelrp  10016  ltxr  10104  divelunit  10331  iccf1o  10334  elfz2  10345  elfzp1  10402  fzdifsuc  10411  fznn  10419  nelfzo  10482  fzosplitsni  10577  fvinim0ffz  10583  infssuzex  10589  zsupssdc  10594  frec2uzisod  10765  sq11i  10987  wrdval  11220  csbwrdg  11247  swrdnd  11344  wrd2ind  11408  cjreb  11544  rexfiuz  11667  cau3lem  11792  pwm1geoserap1  12187  mertensabs  12216  divides  12468  dvdsabseq  12526  odd2np1  12552  oddm1even  12554  modremain  12608  bezoutlemnewy  12685  bezoutlemstep  12686  bezoutlemmain  12687  bezoutlema  12688  bezoutlemb  12689  isprm2  12807  isprm4  12809  dvdsnprmd  12815  oddprmdvds  13045  4sqlem2  13080  4sqlem12  13093  xpsfrnel2  13548  issubm  13674  grplmulf1o  13776  grplactcnv  13804  issubg  13879  elnmz  13914  isghm  13949  ghmeqker  13977  srg1zr  14120  iscrng2  14148  issubrng  14333  aprval  14417  zndvds  14784  znleval  14788  psrbag  14804  istopg  14851  basgen2  14933  isnei  14996  restdis  15036  iscn  15049  iscnp  15051  lmbr2  15066  lmbrf  15067  txcn  15127  cnmpt21  15143  blres  15286  isxms2  15304  metrest  15358  metcnp  15364  txmetcnp  15370  txmetcn  15371  cnblcld  15387  reopnap  15398  ioocosf1o  15706  mpodvdsmulf1o  15845  gausslemma2dlem0i  15917  gausslemma2dlem1a  15918  lgseisenlem2  15931  lgsquadlem1  15937  lgsquadlem2  15938  2lgslem1a  15948  isuhgrm  16053  isushgrm  16054  isupgren  16077  isumgren  16087  isuspgren  16139  isusgren  16140  uhgr0v0e  16216  vtxdg0v  16276  iswlk  16305  wlk1walkdom  16341  istrl  16367  clwwlkn1  16400  clwwlkn2  16403  clwwlknonel  16414  clwwlknun  16423  iseupth  16429  eupthres  16439  eupth2lem1  16440  eupth2lemsfi  16460  bj-nn0sucALT  16735  apdiff  16819