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  4357  opswapg  5174  coexg  5232  iotass  5254  resdif  5551  fvexg  5602  isotr  5892  xpexgALT  6225  ixpssmapg  6822  mapen  6950  mapdom1g  6951  elfir  7082  cauappcvgprlemladdfl  7775  addgt0sr  7895  axmulass  7993  axdistr  7994  negeu  8270  ltaddnegr  8505  nnsub  9082  zltnle  9425  ltsubnn0  9447  elz2  9451  uzaddcl  9714  qaddcl  9763  xltneg  9965  xleneg  9966  iccneg  10118  uzsubsubfz  10176  fzsplit2  10179  fzss1  10192  uzsplit  10221  fz0fzdiffz0  10259  difelfzle  10263  difelfznle  10264  fzonlt0  10298  fzouzsplit  10310  fzo0addelr  10325  eluzgtdifelfzo  10333  elfzodifsumelfzo  10337  ssfzo12  10360  qltnle  10393  modfzo0difsn  10547  nn0ennn  10585  seqfveq2g  10629  ser3mono  10639  iseqf1olemjpcl  10660  iseqf1olemqpcl  10661  seqf1oglem1  10671  seqf1oglem2  10672  seqf1og  10673  fser0const  10687  mulsubdivbinom2ap  10863  faclbnd  10893  bcval4  10904  bcpasc  10918  hashfacen  10988  seq3coll  10994  ccatval1  11061  ccatval21sw  11069  ccatrn  11073  swrd0g  11121  swrdfv2  11124  swrdspsleq  11128  addlenpfx  11150  ccatpfx  11160  swrdswrd  11164  crim  11213  mingeb  11597  fsumshftm  11800  isumshft  11845  cvgratgt0  11888  mertenslemi1  11890  prod1dc  11941  fprod1p  11954  fprodmodd  11996  negdvdsb  12162  dvdsnegb  12163  dvdsmul1  12168  dvdsabseq  12202  dvdsssfz1  12207  odd2np1  12228  ndvdsadd  12286  dvdssqim  12389  nn0seqcvgd  12407  algcvgblem  12415  cncongr2  12470  prmind2  12486  prmdvdsfz  12505  prmndvdsfaclt  12522  dvdsfi  12605  modprm0  12621  modprmn0modprm0  12623  pythagtriplem1  12632  pythagtriplem4  12635  pythagtriplem8  12639  pythagtriplem9  12640  pythagtriplem12  12642  pythagtriplem14  12644  pythagtriplem16  12646  pcexp  12676  pc2dvds  12697  pcz  12699  fldivp1  12715  pcfac  12717  oddprmdvds  12721  pockthg  12724  infpnlem1  12726  1arith  12734  4sqlem11  12768  pwsval  13167  ismgmid  13253  mhmpropd  13342  grpsubid1  13461  mulgnnp1  13510  mulgsubcl  13516  mulgnn0z  13529  mulgnndir  13531  mulgneg2  13536  ghmco  13644  gsumfzfsumlemm  14393  resttopon  14687  cnovex  14712  iscn  14713  iscnp  14715  cnco  14737  cndis  14757  hmeoco  14832  bl2in  14919  metss2lem  15013  metss2  15014  bdxmet  15017  metrest  15022  ioo2bl  15067  expcn  15085  elcncf  15089  dvexp  15227  plypow  15260  relogexp  15388  logcxp  15413  wilthlem1  15496  sgmnncl  15504  mpodvdsmulf1o  15506  lgsdirnn0  15568  gausslemma2dlem1a  15579  lgsquadlem1  15598  lgsquad2  15604  lgsquad3  15605  supfz  16084