Theorem syl2anr 290

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  swopo  4337  opswapg  5152  coexg  5210  iotass  5232  resdif  5522  fvexg  5573  isotr  5859  xpexgALT  6185  ixpssmapg  6782  mapen  6902  mapdom1g  6903  elfir  7032  cauappcvgprlemladdfl  7715  addgt0sr  7835  axmulass  7933  axdistr  7934  negeu  8210  ltaddnegr  8444  nnsub  9021  zltnle  9363  ltsubnn0  9384  elz2  9388  uzaddcl  9651  qaddcl  9700  xltneg  9902  xleneg  9903  iccneg  10055  uzsubsubfz  10113  fzsplit2  10116  fzss1  10129  uzsplit  10158  fz0fzdiffz0  10196  difelfzle  10200  difelfznle  10201  fzonlt0  10234  fzouzsplit  10246  eluzgtdifelfzo  10264  elfzodifsumelfzo  10268  ssfzo12  10291  qltnle  10313  modfzo0difsn  10466  nn0ennn  10504  seqfveq2g  10548  ser3mono  10558  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  seqf1oglem1  10590  seqf1oglem2  10591  seqf1og  10592  fser0const  10606  mulsubdivbinom2ap  10782  faclbnd  10812  bcval4  10823  bcpasc  10837  hashfacen  10907  seq3coll  10913  crim  11002  mingeb  11385  fsumshftm  11588  isumshft  11633  cvgratgt0  11676  mertenslemi1  11678  prod1dc  11729  fprod1p  11742  fprodmodd  11784  negdvdsb  11950  dvdsnegb  11951  dvdsmul1  11956  dvdsabseq  11989  dvdsssfz1  11994  odd2np1  12014  ndvdsadd  12072  dvdssqim  12161  nn0seqcvgd  12179  algcvgblem  12187  cncongr2  12242  prmind2  12258  prmdvdsfz  12277  prmndvdsfaclt  12294  phisum  12378  modprm0  12392  modprmn0modprm0  12394  pythagtriplem1  12403  pythagtriplem4  12406  pythagtriplem8  12410  pythagtriplem9  12411  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem16  12417  pcexp  12447  pc2dvds  12468  pcz  12470  fldivp1  12486  pcfac  12488  oddprmdvds  12492  pockthg  12495  infpnlem1  12497  1arith  12505  4sqlem11  12539  ismgmid  12960  mhmpropd  13038  grpsubid1  13157  mulgnnp1  13200  mulgsubcl  13206  mulgnn0z  13219  mulgnndir  13221  mulgneg2  13226  ghmco  13334  gsumfzfsumlemm  14075  resttopon  14339  cnovex  14364  iscn  14365  iscnp  14367  cnco  14389  cndis  14409  hmeoco  14484  bl2in  14571  metss2lem  14665  metss2  14666  bdxmet  14669  metrest  14674  ioo2bl  14711  elcncf  14728  dvexp  14860  plypow  14890  relogexp  15007  logcxp  15032  wilthlem1  15112  lgsdirnn0  15163  gausslemma2dlem1a  15174  lgsquadlem1  15191  supfz  15561