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  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  3749  ralprg  3759  rexprg  3760  difsn  3850  opthpr  3895  ralunsn  3921  dfiin2g  4043  iunxsng  4086  iunxsngf  4088  elpwuni  4100  pwnss  4294  exmid01  4333  opelopabt  4402  opelopabga  4403  brabga  4404  opelopabgf  4410  elsucg  4547  elsuc2g  4548  brab2a  4826  opeliunxp  4828  posng  4845  brab2ga  4848  csbdmg  4973  elrnmpt1  5031  elrnmptg  5032  eliniseg2  5165  poleloe  5185  elxp4  5273  elxp5  5274  cnvpom  5328  sbcfung  5399  dffun8  5403  fncnv  5445  fununi  5447  fnssresb  5493  fnimaeq0  5503  funcocnv2  5662  dffn5im  5745  funimass4  5750  fnsnfv  5759  dmfco  5770  fndmdif  5808  fndmin  5810  unpreima  5827  respreima  5830  fsn2  5876  fnressn  5895  fressnfv  5896  elunirn  5966  dff13  5968  fliftel  5993  isoini  6018  f1oiso  6026  riotaeqimp  6057  acexmid  6078  fnbrovb  6124  eloprabga  6169  resoprab2  6179  ralrnmpo  6197  rexrnmpo  6198  ovid  6199  ov  6202  ovg  6222  ofrfval2  6313  fmpox  6430  1stconst  6451  2ndconst  6452  f1od2  6465  rbropapd  6507  brtpos2  6516  dfsmo2  6552  frecabcl  6664  brdifun  6828  eqerlem  6832  brecop  6893  erovlem  6895  mapfset  6939  mapsnd  6964  mapsn  6966  mptelixpg  7010  map1  7095  xpsnen  7113  xpdom2  7123  xpf1o  7138  mapunen  7145  supubti  7333  infglbti  7359  ctssdccl  7445  nninfwlpoim  7513  nninfinfwlpo  7514  netap  7614  2omotaplemap  7617  ltpiord  7680  nlt1pig  7702  elinp  7835  ltdfpr  7867  genpassl  7885  genpassu  7886  1idprl  7951  1idpru  7952  gt0srpr  8109  mappsrprg  8165  map2psrprg  8166  peano2nnnn  8214  recidpirq  8219  axprecex  8241  xrlenlt  8384  addsubeq4  8535  renegcl  8581  lesub0  8801  recexaplem2  8974  conjmulap  9053  rerecclap  9054  creui  9284  peano2nn  9299  nndiv  9328  elznn0  9642  eqreznegel  9997  negelrp  10071  ltxr  10160  divelunit  10387  iccf1o  10390  elfz2  10401  elfzp1  10462  fzdifsuc  10471  fznn  10479  nelfzo  10542  fzosplitsni  10637  fvinim0ffz  10643  infssuzex  10649  zsupssdc  10656  frec2uzisod  10827  sq11i  11049  wrdval  11290  csbwrdg  11317  swrdnd  11414  wrd2ind  11478  cjreb  11614  rexfiuz  11738  cau3lem  11863  pwm1geoserap1  12258  mertensabs  12287  divides  12539  dvdsabseq  12597  odd2np1  12623  oddm1even  12625  modremain  12679  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlemmain  12758  bezoutlema  12759  bezoutlemb  12760  isprm2  12878  isprm4  12880  dvdsnprmd  12886  oddprmdvds  13116  4sqlem2  13151  4sqlem12  13164  xpsfrnel2  13650  issubm  13762  grplmulf1o  13862  grplactcnv  13890  issubg  13959  elnmz  13994  isghm  14029  ghmeqker  14057  rng1zrlem  14241  iscrng2  14302  issubrng  14490  aprval  14574  zndvds  14967  znleval  14971  psrbag  15036  istopg  15083  basgen2  15165  isnei  15228  restdis  15268  iscn  15281  iscnp  15283  lmbr2  15298  lmbrf  15299  txcn  15359  cnmpt21  15375  blres  15518  isxms2  15536  metrest  15590  metcnp  15596  txmetcnp  15602  txmetcn  15603  cnblcld  15619  reopnap  15630  ioocosf1o  15938  mpodvdsmulf1o  16087  gausslemma2dlem0i  16159  gausslemma2dlem1a  16160  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  2lgslem1a  16190  isuhgrm  16295  isushgrm  16296  isupgren  16319  isumgren  16329  isuspgren  16381  isusgren  16382  uhgr0v0e  16458  vtxdg0v  16518  iswlk  16547  wlk1walkdom  16583  istrl  16609  clwwlkn1  16642  clwwlkn2  16645  clwwlknonel  16656  clwwlknun  16665  iseupth  16671  eupthres  16681  eupth2lem1  16682  eupth2lemsfi  16702  bj-nn0sucALT  16987  apdiff  17071  ralrals  17123  rexrals  17124  ralals  17129  rexals  17130