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  4244  exmid01  4283  opelopabt  4351  opelopabga  4352  brabga  4353  opelopabgf  4359  elsucg  4496  elsuc2g  4497  brab2a  4774  opeliunxp  4776  posng  4793  brab2ga  4796  csbdmg  4920  elrnmpt1  4978  elrnmptg  4979  eliniseg2  5111  poleloe  5131  elxp4  5219  elxp5  5220  cnvpom  5274  sbcfung  5345  dffun8  5349  fncnv  5390  fununi  5392  fnssresb  5438  fnimaeq0  5448  funcocnv2  5602  dffn5im  5684  funimass4  5689  fnsnfv  5698  dmfco  5707  fndmdif  5745  fndmin  5747  unpreima  5765  respreima  5768  fsn2  5814  fnressn  5832  fressnfv  5833  elunirn  5899  dff13  5901  fliftel  5926  isoini  5951  f1oiso  5959  riotaeqimp  5988  acexmid  6009  fnbrovb  6055  eloprabga  6100  resoprab2  6110  ralrnmpo  6128  rexrnmpo  6129  ovid  6130  ov  6133  ovg  6153  ofrfval2  6244  fmpox  6357  1stconst  6378  2ndconst  6379  f1od2  6392  rbropapd  6399  brtpos2  6408  dfsmo2  6444  frecabcl  6556  brdifun  6720  eqerlem  6724  brecop  6785  erovlem  6787  mapsn  6850  mptelixpg  6894  map1  6978  xpsnen  6993  xpdom2  7003  xpf1o  7018  supubti  7182  infglbti  7208  ctssdccl  7294  nninfwlpoim  7362  nninfinfwlpo  7363  netap  7456  2omotaplemap  7459  ltpiord  7522  nlt1pig  7544  elinp  7677  ltdfpr  7709  genpassl  7727  genpassu  7728  1idprl  7793  1idpru  7794  gt0srpr  7951  mappsrprg  8007  map2psrprg  8008  peano2nnnn  8056  recidpirq  8061  axprecex  8083  xrlenlt  8227  addsubeq4  8377  renegcl  8423  lesub0  8642  recexaplem2  8815  conjmulap  8892  rerecclap  8893  creui  9123  peano2nn  9138  nndiv  9167  elznn0  9477  eqreznegel  9826  negelrp  9900  ltxr  9988  divelunit  10215  iccf1o  10217  elfz2  10228  elfzp1  10285  fzdifsuc  10294  fznn  10302  nelfzo  10365  fzosplitsni  10458  fvinim0ffz  10464  infssuzex  10470  zsupssdc  10475  frec2uzisod  10646  sq11i  10868  wrdval  11092  csbwrdg  11119  swrdnd  11212  wrd2ind  11276  cjreb  11398  rexfiuz  11521  cau3lem  11646  pwm1geoserap1  12040  mertensabs  12069  divides  12321  dvdsabseq  12379  odd2np1  12405  oddm1even  12407  modremain  12461  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlemmain  12540  bezoutlema  12541  bezoutlemb  12542  isprm2  12660  isprm4  12662  dvdsnprmd  12668  oddprmdvds  12898  4sqlem2  12933  4sqlem12  12946  xpsfrnel2  13400  issubm  13526  grplmulf1o  13628  grplactcnv  13656  issubg  13731  elnmz  13766  isghm  13801  ghmeqker  13829  srg1zr  13971  iscrng2  13999  issubrng  14184  aprval  14267  zndvds  14634  znleval  14638  psrbag  14654  istopg  14694  basgen2  14776  isnei  14839  restdis  14879  iscn  14892  iscnp  14894  lmbr2  14909  lmbrf  14910  txcn  14970  cnmpt21  14986  blres  15129  isxms2  15147  metrest  15201  metcnp  15207  txmetcnp  15213  txmetcn  15214  cnblcld  15230  reopnap  15241  ioocosf1o  15549  mpodvdsmulf1o  15685  gausslemma2dlem0i  15757  gausslemma2dlem1a  15758  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  2lgslem1a  15788  isuhgrm  15892  isushgrm  15893  isupgren  15916  isumgren  15926  isuspgren  15976  isusgren  15977  uhgr0v0e  16053  vtxdg0v  16080  iswlk  16095  wlk1walkdom  16131  istrl  16155  clwwlkn1  16186  clwwlkn2  16189  bj-nn0sucALT  16450  apdiff  16530