Theorem sylanb 488

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
sylanb.1	⊢ (𝜑 ↔ 𝜓)
sylanb.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylanb	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylanb

Step	Hyp	Ref	Expression
1		sylanb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 205	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 487	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  syl2anb  495  anabsan  850  eqtr2  2630  pm13.181  2864  rmob  3495  sspsstr  3674  disjne  3974  seex  5001  xpcan2  5490  tron  5663  fssres  5983  funbrfvb  6148  funopfvb  6149  fvco  6184  fvimacnvi  6239  ffvresb  6301  funressn  6331  funresdfunsn  6360  fvtp2  6366  fvtp2g  6369  fnex  6386  funex  6387  ordsucss  6910  ordsucelsuc  6914  1st2nd  7105  frxp  7174  dftpos4  7258  tz7.48lem  7423  nnmsucr  7592  nnmcan  7601  xpmapenlem  8012  php  8029  php4  8032  isfinite2  8103  fundmfibi  8130  fiinfcl  8290  wofib  8333  r1limg  8517  r1pwcl  8593  cardmin2  8707  zornn0g  9210  intgru  9515  supsrlem  9811  nzadd  11302  fnn0ind  11352  uztrn2  11581  nnwo  11629  irradd  11688  qbtwnxr  11905  xltnegi  11921  xaddnemnf  11941  xaddnepnf  11942  xaddcom  11945  xnegdi  11950  elioore  12076  uzsubsubfz1  12235  fzo1fzo0n0  12386  elfzonelfzo  12436  modsumfzodifsn  12605  leexp2  12777  faclbnd  12939  faclbnd3  12941  fi1uzind  13134  brfi1uzind  13135  opfi1uzind  13138  fi1uzindOLD  13140  brfi1uzindOLD  13141  opfi1uzindOLD  13144  swrdccat3b  13347  dvdslelem  14869  divalglem1  14955  isprm2lem  15232  dvdsprime  15238  pcgcd  15420  cntri  17586  efgsrel  17970  xrsdsreclb  19612  znf1o  19719  restuni  20776  stoig  20777  restperf  20798  resstps  20801  pnfnei  20834  mnfnei  20835  cnnei  20896  cmpsublem  21012  comppfsc  21145  tx1stc  21263  xkopt  21268  isfcls  21623  tgioo  22407  opnreen  22442  iscmet3  22899  dyaddisj  23170  limcmpt  23453  degltlem1  23636  ulmdvlem3  23960  lgsdi  24859  clwlkfclwwlk  26371  2wlkonotv  26404  eupath2lem3  26506  grpoidinvlem3  26744  ipasslem3  27072  spanuni  27787  5oalem3  27899  5oalem5  27901  mdslmd1lem2  28569  mptct  28880  mptctf  28883  xaddeq0  28907  ordtconlem1  29298  esumcvg  29475  ldgenpisyslem1  29553  measres  29612  measdivcstOLD  29614  measdivcst  29615  probun  29808  elmpps  30724  dfon2lem9  30940  noreson  31057  funpartfun  31220  cgrxfr  31332  segcon2  31382  brsegle2  31386  seglecgr12im  31387  segletr  31391  nn0prpw  31488  bj-seex  32111  lindsenlbs  32574  matunitlindflem2  32576  ptrecube  32579  poimirlem28  32607  ftc1anclem5  32659  ftc1anc  32663  exlimddvfi  33097  prtlem11  33169  mzpclall  36308  4an31  37725  iundjiun  39353  funbrafvb  39885  funopafvb  39886  afvco2  39905  cusgrres  40664  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  wwlksnred  41098  clwlksfclwwlk  41269  eupth2lem3lem4  41399