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  4338  opswapg  5153  coexg  5211  iotass  5233  resdif  5523  fvexg  5574  isotr  5860  xpexgALT  6187  ixpssmapg  6784  mapen  6904  mapdom1g  6905  elfir  7034  cauappcvgprlemladdfl  7717  addgt0sr  7837  axmulass  7935  axdistr  7936  negeu  8212  ltaddnegr  8446  nnsub  9023  zltnle  9366  ltsubnn0  9387  elz2  9391  uzaddcl  9654  qaddcl  9703  xltneg  9905  xleneg  9906  iccneg  10058  uzsubsubfz  10116  fzsplit2  10119  fzss1  10132  uzsplit  10161  fz0fzdiffz0  10199  difelfzle  10203  difelfznle  10204  fzonlt0  10237  fzouzsplit  10249  eluzgtdifelfzo  10267  elfzodifsumelfzo  10271  ssfzo12  10294  qltnle  10316  modfzo0difsn  10469  nn0ennn  10507  seqfveq2g  10551  ser3mono  10561  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  seqf1oglem1  10593  seqf1oglem2  10594  seqf1og  10595  fser0const  10609  mulsubdivbinom2ap  10785  faclbnd  10815  bcval4  10826  bcpasc  10840  hashfacen  10910  seq3coll  10916  crim  11005  mingeb  11388  fsumshftm  11591  isumshft  11636  cvgratgt0  11679  mertenslemi1  11681  prod1dc  11732  fprod1p  11745  fprodmodd  11787  negdvdsb  11953  dvdsnegb  11954  dvdsmul1  11959  dvdsabseq  11992  dvdsssfz1  11997  odd2np1  12017  ndvdsadd  12075  dvdssqim  12164  nn0seqcvgd  12182  algcvgblem  12190  cncongr2  12245  prmind2  12261  prmdvdsfz  12280  prmndvdsfaclt  12297  phisum  12381  modprm0  12395  modprmn0modprm0  12397  pythagtriplem1  12406  pythagtriplem4  12409  pythagtriplem8  12413  pythagtriplem9  12414  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem16  12420  pcexp  12450  pc2dvds  12471  pcz  12473  fldivp1  12489  pcfac  12491  oddprmdvds  12495  pockthg  12498  infpnlem1  12500  1arith  12508  4sqlem11  12542  ismgmid  12963  mhmpropd  13041  grpsubid1  13160  mulgnnp1  13203  mulgsubcl  13209  mulgnn0z  13222  mulgnndir  13224  mulgneg2  13229  ghmco  13337  gsumfzfsumlemm  14086  resttopon  14350  cnovex  14375  iscn  14376  iscnp  14378  cnco  14400  cndis  14420  hmeoco  14495  bl2in  14582  metss2lem  14676  metss2  14677  bdxmet  14680  metrest  14685  ioo2bl  14730  expcn  14748  elcncf  14752  dvexp  14890  plypow  14923  relogexp  15048  logcxp  15073  wilthlem1  15153  lgsdirnn0  15204  gausslemma2dlem1a  15215  lgsquadlem1  15234  lgsquad2  15240  lgsquad3  15241  supfz  15631