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  3841  sspsstr  4039  disjne  4411  ssexg  5288  rexopabb  5509  seex  5617  xpcan2  6187  tron  6411  fcof  6763  fssres  6778  funbrfvb  6969  funopfvb  6970  fvco  7014  fvimacnvi  7082  ffvresb  7158  funressn  7195  funresdfunsn  7225  fvtp2  7232  fvtp2g  7235  fnex  7254  funex  7256  ordsucss  7863  ordsucelsuc  7867  1st2nd  8084  1stconst  8148  2ndconst  8149  frxp  8175  imacosupp  8264  dftpos4  8300  tz7.48lemOLD  8489  nnmsucr  8672  nnmcan  8681  xpmapenlem  9201  php  9260  php4  9263  isfinite2  9328  fundmfibi  9363  fiinfcl  9532  wofib  9576  r1limg  9815  elwf  9879  r1pwcl  9898  setrec2lem2  10013  cardmin2  10119  zornn0g  10622  mptct  10661  intgru  10938  supsrlem  11235  nzadd  12784  fnn0ind  12838  uztrn2  13024  nnwo  13080  irradd  13141  qbtwnxr  13370  xltnegi  13386  xaddnemnf  13406  xaddnepnf  13407  xaddcom  13410  xnegdi  13418  elioore  13546  uzsubsubfz1  13721  fzo1fzo0n0  13890  elfzonelfzo  13944  modsumfzodifsn  14127  leexp2  14354  faclbnd  14475  faclbnd3  14477  fi1uzind  14693  brfi1uzind  14694  opfi1uzind  14697  swrdccat3b  14931  dvdslelem  16523  divalglem1  16608  dvdsprime  16906  pcgcd  17100  cntri  19597  cntzsgrpcl  19599  efgsrel  19999  ssdifidllem  21691  xrsdsreclb  21772  znf1o  21912  lindsenlbs  22212  matunitlindflem2  23050  restuni  23535  stoig  23536  restperf  23557  resstps  23560  pnfnei  23593  mnfnei  23594  cnnei  23655  cmpsublem  23772  comppfsc  23906  tx1stc  24024  xkopt  24029  isfcls  24383  tgioo  25170  opnreen  25206  iscmet3  25669  dyaddisj  25972  limcmpt  26258  degltlem1  26445  ulmdvlem3  26786  lgsdi  27718  noreson  28074  divsclw  28638  cusgrres  30086  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  wwlksnred  30538  eupth2lem3lem4  30889  grpoidinvlem3  31165  ipasslem3  31492  spanuni  32203  5oalem3  32315  5oalem5  32317  mdslmd1lem2  32985  rnressnsn  33368  mptctf  33405  xaddeq0  33441  xnn0gt0  33457  ssmxidllem  34102  ssmxidl  34103  ordtconnlem1  34667  esumcvg  34829  ldgenpisyslem1  34907  measdivcst  34968  measdivcstALTV  34969  probun  35162  fnrelpredd  35845  fineqvrep  35923  elmpps  36546  dfon2lem9  36768  funpartfun  36922  cgrxfr  37035  segcon2  37085  brsegle2  37089  seglecgr12im  37090  segletr  37094  nn0prpw  37326  mh-inf3f1  37544  bj-seex  38049  relssresb  38195  bj-axreprepsep  38261  bj-prmoore  38306  fvineqsneu  38602  ptrecube  38806  poimirlem28  38834  ftc1anclem5  38883  ftc1anc  38887  exlimddvfi  39320  imadomfi  43318  readvrec  43679  nn0addcom  43792  nn0mulcom  43796  riccrng1  43848  ricdrng1  43858  mzpclall  44004  4an31  45741  cnrefiisplem  47112  iundjiun  47743  funbrafvb  48499  funopafvb  48500  afvco2  48519  dfatbrafv2b  48588  funbrafv22b  48593  funopafv2b  48594  sprsymrelfolem2  48848  uhgrimgrlim  49358  line2xlem  50196  itsclc0xyqsol  50211  f1mo  50295  catprs  50456