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  4426  opswapg  5248  coexg  5306  iotass  5329  resdif  5635  fvexg  5688  isotr  5988  xpexgALT  6325  mapsnd  6922  ixpssmapg  6962  mapen  7098  mapdom1g  7099  elfir  7259  cauappcvgprlemladdfl  7966  addgt0sr  8086  axmulass  8184  axdistr  8185  negeu  8460  ltaddnegr  8695  nnsub  9272  zltnle  9619  ltsubnn0  9641  elz2  9645  uzaddcl  9914  qaddcl  9963  xltneg  10165  xleneg  10166  iccneg  10318  uzsubsubfz  10377  fzsplit2  10380  fzss1  10393  uzsplit  10422  fz0fzdiffz0  10460  difelfzle  10464  difelfznle  10465  fzonlt0  10499  fzouzsplit  10511  fzo0addelr  10530  eluzgtdifelfzo  10538  elfzodifsumelfzo  10542  ssfzo12  10565  qltnle  10599  modfzo0difsn  10753  nn0ennn  10791  seqfveq2g  10835  ser3mono  10845  iseqf1olemjpcl  10866  iseqf1olemqpcl  10867  seqf1oglem1  10877  seqf1oglem2  10878  seqf1og  10879  fser0const  10893  mulsubdivbinom2ap  11069  faclbnd  11099  bcval4  11110  bcpasc  11124  hashfibclem  11199  hashfacen  11201  seq3coll  11207  ccatval1  11278  ccatval21sw  11286  ccatrn  11290  ccatalpha  11294  swrd0g  11345  swrdfv2  11348  swrdspsleq  11352  addlenpfx  11376  ccatpfx  11386  swrdswrd  11390  pfxccatin12lem2  11416  pfxccat3  11419  swrdccat  11420  crim  11536  mingeb  11920  fsumshftm  12124  isumshft  12169  cvgratgt0  12212  mertenslemi1  12214  prod1dc  12265  fprod1p  12278  fprodmodd  12320  negdvdsb  12486  dvdsnegb  12487  dvdsmul1  12492  dvdsabseq  12526  dvdsssfz1  12531  odd2np1  12552  ndvdsadd  12610  dvdssqim  12713  nn0seqcvgd  12731  algcvgblem  12739  cncongr2  12794  prmind2  12810  prmdvdsfz  12829  prmndvdsfaclt  12846  dvdsfi  12929  modprm0  12945  modprmn0modprm0  12947  pythagtriplem1  12956  pythagtriplem4  12959  pythagtriplem8  12963  pythagtriplem9  12964  pythagtriplem12  12966  pythagtriplem14  12968  pythagtriplem16  12970  pcexp  13000  pc2dvds  13021  pcz  13023  fldivp1  13039  pcfac  13041  oddprmdvds  13045  pockthg  13048  infpnlem1  13050  1arith  13058  4sqlem11  13092  pwsval  13493  ismgmid  13579  mhmpropd  13668  grpsubid1  13787  mulgnnp1  13836  mulgsubcl  13842  mulgnn0z  13855  mulgnndir  13857  mulgneg2  13862  ghmco  13970  gsumfzfsumlemm  14722  resttopon  15023  cnovex  15048  iscn  15049  iscnp  15051  cnco  15073  cndis  15093  hmeoco  15168  bl2in  15255  metss2lem  15349  metss2  15350  bdxmet  15353  metrest  15358  ioo2bl  15403  expcn  15421  elcncf  15425  dvexp  15563  plypow  15596  relogexp  15724  logcxp  15749  wilthlem1  15835  sgmnncl  15843  mpodvdsmulf1o  15845  lgsdirnn0  15907  gausslemma2dlem1a  15918  lgsquadlem1  15937  lgsquad2  15943  lgsquad3  15944  uspgrupgrushgr  16164  usgrumgruspgr  16167  wksfval  16304  wlkex  16307  supfz  16843