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 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr2id  193  bitr3id  194  3bitr4g  223  imim21b  253  pm5.17dc  916  dn1dc  973  bilukdc  1445  nf4dc  1722  sbal1  2062  abbibcom  2352  abbib  2356  necon3abid  2459  necon3bid  2461  necon1abiidc  2480  r19.21t  2625  ceqsralt  2849  ceqsrexv  2956  ceqsrex2v  2958  elab2g  2973  elrabf  2980  eueq2dc  2999  euxfrdc  3012  eqreu  3018  reu8  3022  ru  3050  sbcralt  3128  sbcrext  3129  sbcne12g  3165  csbnestgf  3200  dfss4st  3464  rexsng  3750  ralprg  3760  rexprg  3761  difsn  3852  opthpr  3897  ralunsn  3923  dfiin2g  4045  iunxsng  4088  iunxsngf  4090  elpwuni  4102  pwnss  4298  exmid01  4337  opelopabt  4406  opelopabga  4407  brabga  4408  opelopabgf  4414  elsucg  4551  elsuc2g  4552  brab2a  4830  opeliunxp  4832  posng  4849  brab2ga  4852  csbdmg  4977  elrnmpt1  5035  elrnmptg  5036  eliniseg2  5170  poleloe  5190  elxp4  5278  elxp5  5279  cnvpom  5333  sbcfung  5404  dffun8  5408  fncnv  5450  fununi  5452  fnssresb  5498  fnimaeq0  5508  funcocnv2  5667  dffn5im  5751  funimass4  5756  fnsnfv  5765  dmfco  5776  fndmdif  5817  fndmin  5819  unpreima  5836  respreima  5839  fsn2  5885  fnressn  5904  fressnfv  5905  elunirn  5975  dff13  5977  fliftel  6002  isoini  6027  f1oiso  6035  riotaeqimp  6066  acexmid  6087  fnbrovb  6133  eloprabga  6178  resoprab2  6188  ralrnmpo  6206  rexrnmpo  6207  ovid  6208  ov  6211  ovg  6231  ofrfval2  6323  fmpox  6440  1stconst  6461  2ndconst  6462  f1od2  6475  rbropapd  6517  brtpos2  6526  dfsmo2  6562  frecabcl  6674  brdifun  6838  eqerlem  6842  brecop  6903  erovlem  6905  mapfset  6949  mapsnd  6975  mapsn  6977  mptelixpg  7021  map1  7106  xpsnen  7124  xpdom2  7134  xpf1o  7149  mapunen  7156  supubti  7346  infglbti  7372  ctssdccl  7458  nninfwlpoim  7526  nninfinfwlpo  7527  netap  7627  2omotaplemap  7630  ltpiord  7693  nlt1pig  7715  elinp  7848  ltdfpr  7880  genpassl  7898  genpassu  7899  1idprl  7964  1idpru  7965  gt0srpr  8122  mappsrprg  8178  map2psrprg  8179  peano2nnnn  8227  recidpirq  8232  axprecex  8254  xrlenlt  8397  addsubeq4  8549  renegcl  8595  lesub0  8815  recexaplem2  8989  conjmulap  9068  rerecclap  9069  creui  9299  peano2nn  9326  nndiv  9355  elznn0  9671  eqreznegel  10031  negelrp  10106  ltxr  10195  divelunit  10422  iccf1o  10425  elfz2  10436  elfzp1  10497  fzdifsuc  10506  fznn  10514  nelfzo  10577  fzosplitsni  10672  fvinim0ffz  10678  infssuzex  10684  zsupssdc  10691  frec2uzisod  10866  sq11i  11088  nn0sqdc  11169  wrdval  11330  csbwrdg  11357  swrdnd  11454  wrd2ind  11518  cjreb  11654  rexfiuz  11778  cau3lem  11904  pwm1geoserap1  12301  mertensabs  12330  divides  12582  dvdsabseq  12640  odd2np1  12666  oddm1even  12668  modremain  12722  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlemmain  12801  bezoutlema  12802  bezoutlemb  12803  isprm2  12921  isprm4  12923  dvdsnprmd  12929  nnmaxpw  12979  oddprmdvds  13163  4sqlem2  13198  4sqlem12  13211  xpsfrnel2  13727  issubm  13839  grplmulf1o  13939  grplactcnv  13967  issubg  14036  elnmz  14071  isghm  14106  ghmeqker  14134  resscntz  14167  cntzsgrpcl  14168  rng1zrlem  14366  iscrng2  14427  issubrng  14617  aprval  14701  zndvds  15094  znleval  15098  psrbag  15165  istopg  15237  basgen2  15319  isnei  15382  restdis  15422  iscn  15435  iscnp  15437  lmbr2  15452  lmbrf  15453  txcn  15513  cnmpt21  15529  blres  15672  isxms2  15690  metrest  15744  metcnp  15750  txmetcnp  15756  txmetcn  15757  cnblcld  15773  reopnap  15784  sineq0re  16088  ioocosf1o  16094  mpodvdsmulf1o  16296  gausslemma2dlem0i  16393  gausslemma2dlem1a  16394  lgseisenlem2  16407  lgsquadlem1  16413  lgsquadlem2  16414  2lgslem1a  16424  isuhgrm  16529  isushgrm  16530  isupgren  16553  isumgren  16563  isuspgren  16615  isusgren  16616  uhgr0v0e  16692  vtxdg0v  16752  iswlk  16781  wlk1walkdom  16817  istrl  16843  clwwlkn1  16876  clwwlkn2  16879  clwwlknonel  16890  clwwlknun  16899  iseupth  16905  eupthres  16915  eupth2lem1  16916  eupth2lemsfi  16936  bj-nn0sucALT  17221  apdiff  17316  ralrals  17368  rexrals  17369  ralals  17374  rexals  17375