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  suppinisegdc  6513  rbropapd  6518  brtpos2  6527  dfsmo2  6563  frecabcl  6675  brdifun  6839  eqerlem  6843  brecop  6904  erovlem  6906  mapfset  6950  mapsnd  6976  mapsn  6978  mptelixpg  7022  map1  7107  xpsnen  7125  xpdom2  7135  xpf1o  7150  mapunen  7157  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  9669  eqreznegel  10030  negelrp  10105  ltxr  10194  divelunit  10421  iccf1o  10424  elfz2  10435  elfzp1  10496  fzdifsuc  10505  fznn  10513  nelfzo  10576  fzosplitsni  10671  fvinim0ffz  10677  infssuzex  10683  zsupssdc  10690  frec2uzisod  10865  sq11i  11087  nn0sqdc  11168  wrdval  11329  csbwrdg  11356  swrdnd  11453  wrd2ind  11517  cjreb  11653  rexfiuz  11777  cau3lem  11903  pwm1geoserap1  12300  mertensabs  12329  divides  12581  dvdsabseq  12639  odd2np1  12665  oddm1even  12667  modremain  12721  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlema  12801  bezoutlemb  12802  isprm2  12920  isprm4  12922  dvdsnprmd  12928  nnmaxpw  12978  oddprmdvds  13162  4sqlem2  13197  4sqlem12  13210  xpsfrnel2  13726  issubm  13838  grplmulf1o  13938  grplactcnv  13966  issubg  14035  elnmz  14070  isghm  14105  ghmeqker  14133  resscntz  14166  cntzsgrpcl  14167  rng1zrlem  14365  iscrng2  14426  issubrng  14616  aprval  14700  zndvds  15093  znleval  15097  psrbag  15164  istopg  15258  basgen2  15340  isnei  15403  restdis  15443  iscn  15456  iscnp  15458  lmbr2  15473  lmbrf  15474  txcn  15534  cnmpt21  15550  blres  15693  isxms2  15711  metrest  15765  metcnp  15771  txmetcnp  15777  txmetcn  15778  cnblcld  15794  reopnap  15805  sineq0re  16109  ioocosf1o  16115  mpodvdsmulf1o  16317  gausslemma2dlem0i  16414  gausslemma2dlem1a  16415  lgseisenlem2  16428  lgsquadlem1  16434  lgsquadlem2  16435  2lgslem1a  16445  isuhgrm  16550  isushgrm  16551  isupgren  16574  isumgren  16584  isuspgren  16636  isusgren  16637  uhgr0v0e  16713  vtxdg0v  16773  iswlk  16802  wlk1walkdom  16838  istrl  16864  clwwlkn1  16897  clwwlkn2  16900  clwwlknonel  16911  clwwlknun  16920  iseupth  16926  eupthres  16936  eupth2lem1  16937  eupth2lemsfi  16957  bj-nn0sucALT  17242  apdiff  17337  ralrals  17389  rexrals  17390  ralals  17395  rexals  17396