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  4296  exmid01  4335  opelopabt  4404  opelopabga  4405  brabga  4406  opelopabgf  4412  elsucg  4549  elsuc2g  4550  brab2a  4828  opeliunxp  4830  posng  4847  brab2ga  4850  csbdmg  4975  elrnmpt1  5033  elrnmptg  5034  eliniseg2  5167  poleloe  5187  elxp4  5275  elxp5  5276  cnvpom  5330  sbcfung  5401  dffun8  5405  fncnv  5447  fununi  5449  fnssresb  5495  fnimaeq0  5505  funcocnv2  5664  dffn5im  5748  funimass4  5753  fnsnfv  5762  dmfco  5773  fndmdif  5814  fndmin  5816  unpreima  5833  respreima  5836  fsn2  5882  fnressn  5901  fressnfv  5902  elunirn  5972  dff13  5974  fliftel  5999  isoini  6024  f1oiso  6032  riotaeqimp  6063  acexmid  6084  fnbrovb  6130  eloprabga  6175  resoprab2  6185  ralrnmpo  6203  rexrnmpo  6204  ovid  6205  ov  6208  ovg  6228  ofrfval2  6319  fmpox  6436  1stconst  6457  2ndconst  6458  f1od2  6471  rbropapd  6513  brtpos2  6522  dfsmo2  6558  frecabcl  6670  brdifun  6834  eqerlem  6838  brecop  6899  erovlem  6901  mapfset  6945  mapsnd  6970  mapsn  6972  mptelixpg  7016  map1  7101  xpsnen  7119  xpdom2  7129  xpf1o  7144  mapunen  7151  supubti  7339  infglbti  7365  ctssdccl  7451  nninfwlpoim  7519  nninfinfwlpo  7520  netap  7620  2omotaplemap  7623  ltpiord  7686  nlt1pig  7708  elinp  7841  ltdfpr  7873  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  gt0srpr  8115  mappsrprg  8171  map2psrprg  8172  peano2nnnn  8220  recidpirq  8225  axprecex  8247  xrlenlt  8390  addsubeq4  8541  renegcl  8587  lesub0  8807  recexaplem2  8981  conjmulap  9060  rerecclap  9061  creui  9291  peano2nn  9317  nndiv  9346  elznn0  9661  eqreznegel  10016  negelrp  10090  ltxr  10179  divelunit  10406  iccf1o  10409  elfz2  10420  elfzp1  10481  fzdifsuc  10490  fznn  10498  nelfzo  10561  fzosplitsni  10656  fvinim0ffz  10662  infssuzex  10668  zsupssdc  10675  frec2uzisod  10846  sq11i  11068  wrdval  11309  csbwrdg  11336  swrdnd  11433  wrd2ind  11497  cjreb  11633  rexfiuz  11757  cau3lem  11882  pwm1geoserap1  12277  mertensabs  12306  divides  12558  dvdsabseq  12616  odd2np1  12642  oddm1even  12644  modremain  12698  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlemmain  12777  bezoutlema  12778  bezoutlemb  12779  isprm2  12897  isprm4  12899  dvdsnprmd  12905  oddprmdvds  13135  4sqlem2  13170  4sqlem12  13183  xpsfrnel2  13669  issubm  13781  grplmulf1o  13881  grplactcnv  13909  issubg  13978  elnmz  14013  isghm  14048  ghmeqker  14076  rng1zrlem  14260  iscrng2  14321  issubrng  14509  aprval  14593  zndvds  14986  znleval  14990  psrbag  15055  istopg  15102  basgen2  15184  isnei  15247  restdis  15287  iscn  15300  iscnp  15302  lmbr2  15317  lmbrf  15318  txcn  15378  cnmpt21  15394  blres  15537  isxms2  15555  metrest  15609  metcnp  15615  txmetcnp  15621  txmetcn  15622  cnblcld  15638  reopnap  15649  ioocosf1o  15958  mpodvdsmulf1o  16110  gausslemma2dlem0i  16188  gausslemma2dlem1a  16189  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  2lgslem1a  16219  isuhgrm  16324  isushgrm  16325  isupgren  16348  isumgren  16358  isuspgren  16410  isusgren  16411  uhgr0v0e  16487  vtxdg0v  16547  iswlk  16576  wlk1walkdom  16612  istrl  16638  clwwlkn1  16671  clwwlkn2  16674  clwwlknonel  16685  clwwlknun  16694  iseupth  16700  eupthres  16710  eupth2lem1  16711  eupth2lemsfi  16731  bj-nn0sucALT  17016  apdiff  17109  ralrals  17161  rexrals  17162  ralals  17167  rexals  17168