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  4405  opswapg  5225  coexg  5283  iotass  5306  resdif  5608  fvexg  5661  isotr  5962  xpexgALT  6300  ixpssmapg  6902  mapen  7037  mapdom1g  7038  elfir  7177  cauappcvgprlemladdfl  7880  addgt0sr  8000  axmulass  8098  axdistr  8099  negeu  8375  ltaddnegr  8610  nnsub  9187  zltnle  9530  ltsubnn0  9552  elz2  9556  uzaddcl  9825  qaddcl  9874  xltneg  10076  xleneg  10077  iccneg  10229  uzsubsubfz  10287  fzsplit2  10290  fzss1  10303  uzsplit  10332  fz0fzdiffz0  10370  difelfzle  10374  difelfznle  10375  fzonlt0  10409  fzouzsplit  10421  fzo0addelr  10440  eluzgtdifelfzo  10448  elfzodifsumelfzo  10452  ssfzo12  10475  qltnle  10509  modfzo0difsn  10663  nn0ennn  10701  seqfveq2g  10745  ser3mono  10755  iseqf1olemjpcl  10776  iseqf1olemqpcl  10777  seqf1oglem1  10787  seqf1oglem2  10788  seqf1og  10789  fser0const  10803  mulsubdivbinom2ap  10979  faclbnd  11009  bcval4  11020  bcpasc  11034  hashfacen  11106  seq3coll  11112  ccatval1  11183  ccatval21sw  11191  ccatrn  11195  ccatalpha  11199  swrd0g  11250  swrdfv2  11253  swrdspsleq  11257  addlenpfx  11281  ccatpfx  11291  swrdswrd  11295  pfxccatin12lem2  11321  pfxccat3  11324  swrdccat  11325  crim  11441  mingeb  11825  fsumshftm  12029  isumshft  12074  cvgratgt0  12117  mertenslemi1  12119  prod1dc  12170  fprod1p  12183  fprodmodd  12225  negdvdsb  12391  dvdsnegb  12392  dvdsmul1  12397  dvdsabseq  12431  dvdsssfz1  12436  odd2np1  12457  ndvdsadd  12515  dvdssqim  12618  nn0seqcvgd  12636  algcvgblem  12644  cncongr2  12699  prmind2  12715  prmdvdsfz  12734  prmndvdsfaclt  12751  dvdsfi  12834  modprm0  12850  modprmn0modprm0  12852  pythagtriplem1  12861  pythagtriplem4  12864  pythagtriplem8  12868  pythagtriplem9  12869  pythagtriplem12  12871  pythagtriplem14  12873  pythagtriplem16  12875  pcexp  12905  pc2dvds  12926  pcz  12928  fldivp1  12944  pcfac  12946  oddprmdvds  12950  pockthg  12953  infpnlem1  12955  1arith  12963  4sqlem11  12997  pwsval  13397  ismgmid  13483  mhmpropd  13572  grpsubid1  13691  mulgnnp1  13740  mulgsubcl  13746  mulgnn0z  13759  mulgnndir  13761  mulgneg2  13766  ghmco  13874  gsumfzfsumlemm  14625  resttopon  14924  cnovex  14949  iscn  14950  iscnp  14952  cnco  14974  cndis  14994  hmeoco  15069  bl2in  15156  metss2lem  15250  metss2  15251  bdxmet  15254  metrest  15259  ioo2bl  15304  expcn  15322  elcncf  15326  dvexp  15464  plypow  15497  relogexp  15625  logcxp  15650  wilthlem1  15733  sgmnncl  15741  mpodvdsmulf1o  15743  lgsdirnn0  15805  gausslemma2dlem1a  15816  lgsquadlem1  15835  lgsquad2  15841  lgsquad3  15842  uspgrupgrushgr  16062  usgrumgruspgr  16065  wksfval  16202  wlkex  16205  supfz  16743