Theorem syl2anr 284

Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.)

Hypotheses

Ref	Expression
syl2an.1	⊢ (𝜑 → 𝜓)
syl2an.2	⊢ (𝜏 → 𝜒)
syl2an.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anr	⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Proof of Theorem syl2anr

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2an.2	. . 3 ⊢ (𝜏 → 𝜒)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	1, 2, 3	syl2an 283	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 264	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  swopo  4097  opswapg  4871  coexg  4929  iotass  4951  resdif  5223  fvexg  5269  isotr  5535  xpexgALT  5839  mapen  6492  mapdom1g  6493  cauappcvgprlemladdfl  7117  addgt0sr  7224  axmulass  7311  axdistr  7312  negeu  7576  ltaddnegr  7806  nnsub  8354  zltnle  8692  elz2  8714  uzaddcl  8969  qaddcl  9015  xltneg  9193  xleneg  9194  iccneg  9301  uzsubsubfz  9356  fzsplit2  9359  fzss1  9371  uzsplit  9399  fz0fzdiffz0  9432  difelfzle  9436  difelfznle  9437  fzonlt0  9467  fzouzsplit  9479  eluzgtdifelfzo  9497  elfzodifsumelfzo  9501  ssfzo12  9524  qltnle  9546  modfzo0difsn  9691  nn0ennn  9729  isermono  9772  faclbnd  9984  bcval4  9995  bcpasc  10009  hashfacen  10075  crim  10119  negdvdsb  10592  dvdsnegb  10593  dvdsmul1  10598  dvdsabseq  10628  dvdsssfz1  10633  odd2np1  10653  ndvdsadd  10711  dvdssqim  10793  nn0seqcvgd  10803  algcvgblem  10811  cncongr2  10866  prmind2  10882  prmdvdsfz  10900  prmndvdsfaclt  10915