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  911  dn1dc  968  bilukdc  1440  nf4dc  1718  sbal1  2055  abbi  2345  necon3abid  2441  necon3bid  2443  necon1abiidc  2462  r19.21t  2607  ceqsralt  2830  ceqsrexv  2936  ceqsrex2v  2938  elab2g  2953  elrabf  2960  eueq2dc  2979  euxfrdc  2992  eqreu  2998  reu8  3002  ru  3030  sbcralt  3108  sbcrext  3109  sbcne12g  3145  csbnestgf  3180  dfss4st  3440  rexsng  3710  ralprg  3720  rexprg  3721  difsn  3810  opthpr  3855  ralunsn  3881  dfiin2g  4003  iunxsng  4046  iunxsngf  4048  elpwuni  4060  pwnss  4249  exmid01  4288  opelopabt  4356  opelopabga  4357  brabga  4358  opelopabgf  4364  elsucg  4501  elsuc2g  4502  brab2a  4779  opeliunxp  4781  posng  4798  brab2ga  4801  csbdmg  4925  elrnmpt1  4983  elrnmptg  4984  eliniseg2  5116  poleloe  5136  elxp4  5224  elxp5  5225  cnvpom  5279  sbcfung  5350  dffun8  5354  fncnv  5396  fununi  5398  fnssresb  5444  fnimaeq0  5454  funcocnv2  5608  dffn5im  5691  funimass4  5696  fnsnfv  5705  dmfco  5714  fndmdif  5752  fndmin  5754  unpreima  5772  respreima  5775  fsn2  5821  fnressn  5840  fressnfv  5841  elunirn  5907  dff13  5909  fliftel  5934  isoini  5959  f1oiso  5967  riotaeqimp  5996  acexmid  6017  fnbrovb  6063  eloprabga  6108  resoprab2  6118  ralrnmpo  6136  rexrnmpo  6137  ovid  6138  ov  6141  ovg  6161  ofrfval2  6252  fmpox  6365  1stconst  6386  2ndconst  6387  f1od2  6400  rbropapd  6408  brtpos2  6417  dfsmo2  6453  frecabcl  6565  brdifun  6729  eqerlem  6733  brecop  6794  erovlem  6796  mapsn  6859  mptelixpg  6903  map1  6987  xpsnen  7005  xpdom2  7015  xpf1o  7030  supubti  7198  infglbti  7224  ctssdccl  7310  nninfwlpoim  7378  nninfinfwlpo  7379  netap  7473  2omotaplemap  7476  ltpiord  7539  nlt1pig  7561  elinp  7694  ltdfpr  7726  genpassl  7744  genpassu  7745  1idprl  7810  1idpru  7811  gt0srpr  7968  mappsrprg  8024  map2psrprg  8025  peano2nnnn  8073  recidpirq  8078  axprecex  8100  xrlenlt  8244  addsubeq4  8394  renegcl  8440  lesub0  8659  recexaplem2  8832  conjmulap  8909  rerecclap  8910  creui  9140  peano2nn  9155  nndiv  9184  elznn0  9494  eqreznegel  9848  negelrp  9922  ltxr  10010  divelunit  10237  iccf1o  10239  elfz2  10250  elfzp1  10307  fzdifsuc  10316  fznn  10324  nelfzo  10387  fzosplitsni  10482  fvinim0ffz  10488  infssuzex  10494  zsupssdc  10499  frec2uzisod  10670  sq11i  10892  wrdval  11117  csbwrdg  11144  swrdnd  11241  wrd2ind  11305  cjreb  11428  rexfiuz  11551  cau3lem  11676  pwm1geoserap1  12071  mertensabs  12100  divides  12352  dvdsabseq  12410  odd2np1  12436  oddm1even  12438  modremain  12492  bezoutlemnewy  12569  bezoutlemstep  12570  bezoutlemmain  12571  bezoutlema  12572  bezoutlemb  12573  isprm2  12691  isprm4  12693  dvdsnprmd  12699  oddprmdvds  12929  4sqlem2  12964  4sqlem12  12977  xpsfrnel2  13431  issubm  13557  grplmulf1o  13659  grplactcnv  13687  issubg  13762  elnmz  13797  isghm  13832  ghmeqker  13860  srg1zr  14003  iscrng2  14031  issubrng  14216  aprval  14299  zndvds  14666  znleval  14670  psrbag  14686  istopg  14726  basgen2  14808  isnei  14871  restdis  14911  iscn  14924  iscnp  14926  lmbr2  14941  lmbrf  14942  txcn  15002  cnmpt21  15018  blres  15161  isxms2  15179  metrest  15233  metcnp  15239  txmetcnp  15245  txmetcn  15246  cnblcld  15262  reopnap  15273  ioocosf1o  15581  mpodvdsmulf1o  15717  gausslemma2dlem0i  15789  gausslemma2dlem1a  15790  lgseisenlem2  15803  lgsquadlem1  15809  lgsquadlem2  15810  2lgslem1a  15820  isuhgrm  15925  isushgrm  15926  isupgren  15949  isumgren  15959  isuspgren  16011  isusgren  16012  uhgr0v0e  16088  vtxdg0v  16148  iswlk  16177  wlk1walkdom  16213  istrl  16239  clwwlkn1  16272  clwwlkn2  16275  clwwlknonel  16286  clwwlknun  16295  iseupth  16301  eupthres  16311  eupth2lem1  16312  eupth2lemsfi  16332  bj-nn0sucALT  16594  apdiff  16673