Theorem sylancom 424

Description: Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.)

Hypotheses

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

Assertion

Ref	Expression
sylancom	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem sylancom

Step	Hyp	Ref	Expression
1		sylancom.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		simpr 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		sylancom.2	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃)
4	1, 2, 3	syl2anc 415	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem is used by:  ordin  4530  fimacnvdisj  5576  fvimacnv  5824  ssct  7114  f1vrnfibi  7259  inl11  7406  ctssdc  7454  enomnilem  7479  enmkvlem  7502  djuen  7568  cauappcvgprlemlol  8015  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemlol  8038  caucvgprlemladdrl  8046  caucvgprprlemlol  8066  suplocsrlem  8176  recgt1i  9231  avgle2  9552  eluzmn  9938  xnn0le2is012  10279  ioodisj  10406  fzneuz  10519  zsupcllemstep  10673  fihashfn  11256  sseqn  11295  shftfvalg  11599  shftfval  11602  cvg1nlemres  11767  resqrexlem1arp  11787  maxabslemval  11991  xrmaxiflemval  12035  xrmaxadd  12046  xrminmax  12050  summodclem3  12166  fsumsplit  12193  mertenslemub  12320  fprodsplit  12383  demoivreALT  12560  bitsp1  12737  gcdneg  12778  bezoutlemsup  12805  eucalginv  12853  eucalg  12856  odzdvds  13047  pclemdc  13090  fldivp1  13150  prmunb  13164  ballotfilemirc  13327  enctlem  13375  ctiunctlemfo  13382  intopsn  13740  grpsubval  13904  mulgnndir  14007  cntzidss  14166  gzsumreidx  14225  gsumvalfi  14236  gsumf1ofi  14244  pwssnf1o  14295  znunit  15078  iscnp4  15410  cnntr  15417  tx2cn  15462  hmeontr  15505  hmeores  15507  xmetres2  15571  metres2  15573  limccnp2cntop  15869  limccoap  15870  birthdaylem3  16188  isomninnlem  17245  iswomninnlem  17266  ismkvnnlem  17269