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  4133  opswapg  4917  coexg  4975  iotass  4997  resdif  5275  fvexg  5324  isotr  5595  xpexgALT  5904  mapen  6562  mapdom1g  6563  cauappcvgprlemladdfl  7214  addgt0sr  7321  axmulass  7408  axdistr  7409  negeu  7673  ltaddnegr  7903  nnsub  8461  zltnle  8796  elz2  8818  uzaddcl  9074  qaddcl  9120  xltneg  9298  xleneg  9299  iccneg  9406  uzsubsubfz  9461  fzsplit2  9464  fzss1  9477  uzsplit  9506  fz0fzdiffz0  9541  difelfzle  9545  difelfznle  9546  fzonlt0  9578  fzouzsplit  9590  eluzgtdifelfzo  9608  elfzodifsumelfzo  9612  ssfzo12  9635  qltnle  9657  modfzo0difsn  9802  nn0ennn  9840  isermono  9906  iseqf1olemjpcl  9924  iseqf1olemqpcl  9925  fser0const  9951  faclbnd  10149  bcval4  10160  bcpasc  10174  hashfacen  10241  iseqcoll  10247  crim  10292  fsum3  10779  fsumshftm  10839  isumshft  10884  cvgratgt0  10927  mertenslemi1  10929  negdvdsb  11090  dvdsnegb  11091  dvdsmul1  11096  dvdsabseq  11126  dvdsssfz1  11131  odd2np1  11151  ndvdsadd  11209  dvdssqim  11291  nn0seqcvgd  11301  algcvgblem  11309  cncongr2  11364  prmind2  11380  prmdvdsfz  11398  prmndvdsfaclt  11413  elcncf  11629  supfz  11916