Theorem sylanb 593

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 219	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 592	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl2anb  610  anabsan  678  rmob  3837  sspsstr  4057  disjne  4408  ssexg  5284  rexopabb  5506  seex  5614  xpcan2  6170  tron  6380  fcof  6726  fssres  6741  funbrfvb  6931  funopfvb  6932  fvco  6976  fvimacnvi  7044  ffvresb  7119  funressn  7156  funresdfunsn  7187  fvtp2  7194  fvtp2g  7197  fnex  7216  funex  7218  ordsucss  7814  ordsucelsuc  7818  1st2nd  8036  1stconst  8097  2ndconst  8098  frxp  8124  imacosupp  8207  dftpos4  8243  tz7.48lem  8430  nnmsucr  8613  nnmcan  8622  xpmapenlem  9142  php  9201  php4  9204  isfinite2  9268  fundmfibi  9303  fiinfcl  9473  wofib  9517  r1limg  9753  r1pwcl  9829  cardmin2  10004  zornn0g  10507  mptct  10546  intgru  10823  supsrlem  11120  nzadd  12666  fnn0ind  12720  uztrn2  12906  nnwo  12962  irradd  13023  qbtwnxr  13252  xltnegi  13268  xaddnemnf  13288  xaddnepnf  13289  xaddcom  13292  xnegdi  13300  elioore  13428  uzsubsubfz1  13602  fzo1fzo0n0  13771  elfzonelfzo  13825  modsumfzodifsn  14008  leexp2  14235  faclbnd  14354  faclbnd3  14356  fi1uzind  14572  brfi1uzind  14573  opfi1uzind  14576  swrdccat3b  14809  dvdslelem  16399  divalglem1  16484  dvdsprime  16777  pcgcd  16970  cntri  19459  cntzsgrpcl  19461  efgsrel  19861  ssdifidllem  21547  xrsdsreclb  21627  znf1o  21764  lindsenlbs  22064  matunitlindflem2  22902  restuni  23387  stoig  23388  restperf  23409  resstps  23412  pnfnei  23445  mnfnei  23446  cnnei  23507  cmpsublem  23624  comppfsc  23758  tx1stc  23876  xkopt  23881  isfcls  24235  tgioo  25022  opnreen  25058  iscmet3  25521  dyaddisj  25824  limcmpt  26110  degltlem1  26297  ulmdvlem3  26638  lgsdi  27570  noreson  27896  divsclw  28460  cusgrres  29908  crctcshwlkn0lem4  30281  crctcshwlkn0lem5  30282  wwlksnred  30360  eupth2lem3lem4  30711  grpoidinvlem3  30987  ipasslem3  31314  spanuni  32025  5oalem3  32137  5oalem5  32139  mdslmd1lem2  32807  rnressnsn  33150  mptctf  33187  xaddeq0  33224  xnn0gt0  33240  ssmxidllem  33876  ssmxidl  33877  ordtconnlem1  34434  esumcvg  34596  ldgenpisyslem1  34674  measdivcst  34735  measdivcstALTV  34736  probun  34930  fnrelpredd  35596  elwf  35604  r1omhf  35614  fineqvrep  35640  elmpps  36152  dfon2lem9  36368  funpartfun  36522  cgrxfr  36635  segcon2  36685  brsegle2  36689  seglecgr12im  36690  segletr  36694  nn0prpw  36942  bj-seex  37665  bj-axreprepsep  37820  bj-prmoore  37865  fvineqsneu  38165  ptrecube  38369  poimirlem28  38397  ftc1anclem5  38446  ftc1anc  38450  exlimddvfi  38870  imadomfi  42868  readvrec  43237  nn0addcom  43350  nn0mulcom  43354  riccrng1  43403  ricdrng1  43410  mzpclall  43572  4an31  45321  cnrefiisplem  46657  iundjiun  47288  funbrafvb  48044  funopafvb  48045  afvco2  48064  dfatbrafv2b  48133  funbrafv22b  48138  funopafv2b  48139  sprsymrelfolem2  48393  uhgrimgrlim  48903  line2xlem  49683  itsclc0xyqsol  49698  f1mo  49781  catprs  49937  setrec2lem2  50620