Theorem sylancom 420

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 411	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ordin  4476  fimacnvdisj  5512  fvimacnv  5752  ssct  6983  f1vrnfibi  7123  inl11  7243  ctssdc  7291  enomnilem  7316  enmkvlem  7339  djuen  7404  cauappcvgprlemlol  7845  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemlol  7868  caucvgprlemladdrl  7876  caucvgprprlemlol  7896  suplocsrlem  8006  recgt1i  9056  avgle2  9364  eluzmn  9740  xnn0le2is012  10074  ioodisj  10201  fzneuz  10309  zsupcllemstep  10461  fihashfn  11034  shftfvalg  11344  shftfval  11347  cvg1nlemres  11511  resqrexlem1arp  11531  maxabslemval  11734  xrmaxiflemval  11776  xrmaxadd  11787  xrminmax  11791  summodclem3  11906  fsumsplit  11933  mertenslemub  12060  fprodsplit  12123  demoivreALT  12300  bitsp1  12477  gcdneg  12518  bezoutlemsup  12545  eucalginv  12593  eucalg  12596  odzdvds  12783  pclemdc  12826  fldivp1  12886  prmunb  12900  enctlem  13018  ctiunctlemfo  13025  pwssnf1o  13346  intopsn  13415  grpsubval  13594  mulgnndir  13703  gsumfzreidx  13889  gsumfzmptfidmadd  13891  znunit  14638  iscnp4  14907  cnntr  14914  tx2cn  14959  hmeontr  15002  hmeores  15004  xmetres2  15068  metres2  15070  limccnp2cntop  15366  limccoap  15367  isomninnlem  16458  iswomninnlem  16477  ismkvnnlem  16480