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  912  dn1dc  969  bilukdc  1441  nf4dc  1718  sbal1  2058  abbibcom  2348  abbib  2352  necon3abid  2453  necon3bid  2455  necon1abiidc  2474  r19.21t  2619  ceqsralt  2843  ceqsrexv  2950  ceqsrex2v  2952  elab2g  2967  elrabf  2974  eueq2dc  2993  euxfrdc  3006  eqreu  3012  reu8  3016  ru  3044  sbcralt  3122  sbcrext  3123  sbcne12g  3159  csbnestgf  3194  dfss4st  3458  rexsng  3736  ralprg  3746  rexprg  3747  difsn  3837  opthpr  3882  ralunsn  3908  dfiin2g  4030  iunxsng  4073  iunxsngf  4075  elpwuni  4087  pwnss  4278  exmid01  4317  opelopabt  4386  opelopabga  4387  brabga  4388  opelopabgf  4394  elsucg  4531  elsuc2g  4532  brab2a  4809  opeliunxp  4811  posng  4828  brab2ga  4831  csbdmg  4956  elrnmpt1  5014  elrnmptg  5015  eliniseg2  5148  poleloe  5168  elxp4  5256  elxp5  5257  cnvpom  5311  sbcfung  5382  dffun8  5386  fncnv  5428  fununi  5430  fnssresb  5476  fnimaeq0  5486  funcocnv2  5645  dffn5im  5728  funimass4  5733  fnsnfv  5742  dmfco  5751  fndmdif  5789  fndmin  5791  unpreima  5808  respreima  5811  fsn2  5857  fnressn  5876  fressnfv  5877  elunirn  5946  dff13  5948  fliftel  5973  isoini  5998  f1oiso  6006  riotaeqimp  6037  acexmid  6058  fnbrovb  6104  eloprabga  6149  resoprab2  6159  ralrnmpo  6177  rexrnmpo  6178  ovid  6179  ov  6182  ovg  6202  ofrfval2  6293  fmpox  6410  1stconst  6431  2ndconst  6432  f1od2  6445  rbropapd  6487  brtpos2  6496  dfsmo2  6532  frecabcl  6644  brdifun  6808  eqerlem  6812  brecop  6873  erovlem  6875  mapsnd  6937  mapsn  6939  mptelixpg  6983  map1  7068  xpsnen  7086  xpdom2  7096  xpf1o  7111  mapunen  7118  supubti  7304  infglbti  7330  ctssdccl  7416  nninfwlpoim  7484  nninfinfwlpo  7485  netap  7585  2omotaplemap  7588  ltpiord  7651  nlt1pig  7673  elinp  7806  ltdfpr  7838  genpassl  7856  genpassu  7857  1idprl  7922  1idpru  7923  gt0srpr  8080  mappsrprg  8136  map2psrprg  8137  peano2nnnn  8185  recidpirq  8190  axprecex  8212  xrlenlt  8355  addsubeq4  8506  renegcl  8552  lesub0  8772  recexaplem2  8945  conjmulap  9024  rerecclap  9025  creui  9255  peano2nn  9270  nndiv  9299  elznn0  9613  eqreznegel  9968  negelrp  10042  ltxr  10131  divelunit  10358  iccf1o  10361  elfz2  10372  elfzp1  10432  fzdifsuc  10441  fznn  10449  nelfzo  10512  fzosplitsni  10607  fvinim0ffz  10613  infssuzex  10619  zsupssdc  10626  frec2uzisod  10797  sq11i  11019  wrdval  11256  csbwrdg  11283  swrdnd  11380  wrd2ind  11444  cjreb  11580  rexfiuz  11704  cau3lem  11829  pwm1geoserap1  12224  mertensabs  12253  divides  12505  dvdsabseq  12563  odd2np1  12589  oddm1even  12591  modremain  12645  bezoutlemnewy  12722  bezoutlemstep  12723  bezoutlemmain  12724  bezoutlema  12725  bezoutlemb  12726  isprm2  12844  isprm4  12846  dvdsnprmd  12852  oddprmdvds  13082  4sqlem2  13117  4sqlem12  13130  xpsfrnel2  13615  issubm  13732  grplmulf1o  13834  grplactcnv  13862  issubg  13931  elnmz  13966  isghm  14001  ghmeqker  14029  rng1zrlem  14203  iscrng2  14263  issubrng  14450  aprval  14534  zndvds  14928  znleval  14932  psrbag  14948  istopg  14995  basgen2  15077  isnei  15140  restdis  15180  iscn  15193  iscnp  15195  lmbr2  15210  lmbrf  15211  txcn  15271  cnmpt21  15287  blres  15430  isxms2  15448  metrest  15502  metcnp  15508  txmetcnp  15514  txmetcn  15515  cnblcld  15531  reopnap  15542  ioocosf1o  15850  mpodvdsmulf1o  15989  gausslemma2dlem0i  16061  gausslemma2dlem1a  16062  lgseisenlem2  16075  lgsquadlem1  16081  lgsquadlem2  16082  2lgslem1a  16092  isuhgrm  16197  isushgrm  16198  isupgren  16221  isumgren  16231  isuspgren  16283  isusgren  16284  uhgr0v0e  16360  vtxdg0v  16420  iswlk  16449  wlk1walkdom  16485  istrl  16511  clwwlkn1  16544  clwwlkn2  16547  clwwlknonel  16558  clwwlknun  16567  iseupth  16573  eupthres  16583  eupth2lem1  16584  eupth2lemsfi  16604  bj-nn0sucALT  16889  apdiff  16973