Theorem syl2anr 288

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 287	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 266	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  swopo  4236  opswapg  5033  coexg  5091  iotass  5113  resdif  5397  fvexg  5448  isotr  5725  xpexgALT  6039  ixpssmapg  6630  mapen  6748  mapdom1g  6749  elfir  6869  cauappcvgprlemladdfl  7487  addgt0sr  7607  axmulass  7705  axdistr  7706  negeu  7977  ltaddnegr  8211  nnsub  8783  zltnle  9124  elz2  9146  uzaddcl  9408  qaddcl  9454  xltneg  9649  xleneg  9650  iccneg  9802  uzsubsubfz  9858  fzsplit2  9861  fzss1  9874  uzsplit  9903  fz0fzdiffz0  9938  difelfzle  9942  difelfznle  9943  fzonlt0  9975  fzouzsplit  9987  eluzgtdifelfzo  10005  elfzodifsumelfzo  10009  ssfzo12  10032  qltnle  10054  modfzo0difsn  10199  nn0ennn  10237  ser3mono  10282  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  fser0const  10320  faclbnd  10519  bcval4  10530  bcpasc  10544  hashfacen  10611  seq3coll  10617  crim  10662  fsumshftm  11246  isumshft  11291  cvgratgt0  11334  mertenslemi1  11336  negdvdsb  11545  dvdsnegb  11546  dvdsmul1  11551  dvdsabseq  11581  dvdsssfz1  11586  odd2np1  11606  ndvdsadd  11664  dvdssqim  11748  nn0seqcvgd  11758  algcvgblem  11766  cncongr2  11821  prmind2  11837  prmdvdsfz  11855  prmndvdsfaclt  11870  resttopon  12379  cnovex  12404  iscn  12405  iscnp  12407  cnco  12429  cndis  12449  hmeoco  12524  bl2in  12611  metss2lem  12705  metss2  12706  bdxmet  12709  metrest  12714  ioo2bl  12751  elcncf  12768  dvexp  12883  relogexp  13001  logcxp  13026  supfz  13428