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  3844  sspsstr  4064  disjne  4415  ssexg  5292  rexopabb  5514  seex  5622  xpcan2  6177  tron  6387  fcof  6733  fssres  6748  funbrfvb  6938  funopfvb  6939  fvco  6983  fvimacnvi  7051  ffvresb  7125  funressn  7160  funresdfunsn  7191  fvtp2  7198  fvtp2g  7201  fnex  7219  funex  7221  ordsucss  7816  ordsucelsuc  7820  1st2nd  8038  1stconst  8097  2ndconst  8098  frxp  8124  imacosupp  8207  dftpos4  8243  tz7.48lem  8430  nnmsucr  8613  nnmcan  8622  xpmapenlem  9135  php  9194  php4  9197  isfinite2  9261  fundmfibi  9296  fiinfcl  9466  wofib  9510  r1limg  9746  r1pwcl  9822  cardmin2  9997  zornn0g  10500  mptct  10533  intgru  10810  supsrlem  11107  nzadd  12653  fnn0ind  12707  uztrn2  12893  nnwo  12949  irradd  13009  qbtwnxr  13238  xltnegi  13254  xaddnemnf  13274  xaddnepnf  13275  xaddcom  13278  xnegdi  13286  elioore  13414  uzsubsubfz1  13588  fzo1fzo0n0  13757  elfzonelfzo  13811  modsumfzodifsn  13994  leexp2  14221  faclbnd  14340  faclbnd3  14342  fi1uzind  14558  brfi1uzind  14559  opfi1uzind  14562  swrdccat3b  14795  dvdslelem  16385  divalglem1  16470  dvdsprime  16763  pcgcd  16956  cntri  19426  cntzsgrpcl  19428  efgsrel  19828  ssdifidllem  21514  xrsdsreclb  21594  znf1o  21731  restuni  23349  stoig  23350  restperf  23371  resstps  23374  pnfnei  23407  mnfnei  23408  cnnei  23469  cmpsublem  23586  comppfsc  23720  tx1stc  23838  xkopt  23843  isfcls  24197  tgioo  24984  opnreen  25020  iscmet3  25483  dyaddisj  25786  limcmpt  26073  degltlem1  26260  ulmdvlem3  26596  lgsdi  27529  noreson  27855  divsclw  28419  cusgrres  29832  crctcshwlkn0lem4  30205  crctcshwlkn0lem5  30206  wwlksnred  30284  eupth2lem3lem4  30629  grpoidinvlem3  30905  ipasslem3  31232  spanuni  31943  5oalem3  32055  5oalem5  32057  mdslmd1lem2  32725  rnressnsn  33069  mptctf  33107  xaddeq0  33144  xnn0gt0  33160  ssmxidllem  33796  ssmxidl  33797  ordtconnlem1  34354  esumcvg  34516  ldgenpisyslem1  34594  measdivcst  34655  measdivcstALTV  34656  probun  34850  fnrelpredd  35516  elwf  35524  r1omhf  35534  fineqvrep  35560  elmpps  36078  dfon2lem9  36294  funpartfun  36448  cgrxfr  36560  segcon2  36610  brsegle2  36614  seglecgr12im  36615  segletr  36619  nn0prpw  36867  bj-seex  37590  bj-axreprepsep  37745  bj-prmoore  37790  fvineqsneu  38090  lindsenlbs  38299  matunitlindflem2  38301  ptrecube  38304  poimirlem28  38332  ftc1anclem5  38381  ftc1anc  38385  exlimddvfi  38804  imadomfi  42802  readvrec  43156  nn0addcom  43269  nn0mulcom  43273  riccrng1  43322  ricdrng1  43329  mzpclall  43491  4an31  45240  cnrefiisplem  46576  iundjiun  47207  funbrafvb  47926  funopafvb  47927  afvco2  47946  dfatbrafv2b  48015  funbrafv22b  48020  funopafv2b  48021  sprsymrelfolem2  48275  uhgrimgrlim  48785  line2xlem  49566  itsclc0xyqsol  49581  f1mo  49664  catprs  49822  setrec2lem2  50505