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  4342  opswapg  5157  coexg  5215  iotass  5237  resdif  5529  fvexg  5580  isotr  5866  xpexgALT  6199  ixpssmapg  6796  mapen  6916  mapdom1g  6917  elfir  7048  cauappcvgprlemladdfl  7741  addgt0sr  7861  axmulass  7959  axdistr  7960  negeu  8236  ltaddnegr  8471  nnsub  9048  zltnle  9391  ltsubnn0  9412  elz2  9416  uzaddcl  9679  qaddcl  9728  xltneg  9930  xleneg  9931  iccneg  10083  uzsubsubfz  10141  fzsplit2  10144  fzss1  10157  uzsplit  10186  fz0fzdiffz0  10224  difelfzle  10228  difelfznle  10229  fzonlt0  10262  fzouzsplit  10274  eluzgtdifelfzo  10292  elfzodifsumelfzo  10296  ssfzo12  10319  qltnle  10352  modfzo0difsn  10506  nn0ennn  10544  seqfveq2g  10588  ser3mono  10598  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  seqf1oglem1  10630  seqf1oglem2  10631  seqf1og  10632  fser0const  10646  mulsubdivbinom2ap  10822  faclbnd  10852  bcval4  10863  bcpasc  10877  hashfacen  10947  seq3coll  10953  crim  11042  mingeb  11426  fsumshftm  11629  isumshft  11674  cvgratgt0  11717  mertenslemi1  11719  prod1dc  11770  fprod1p  11783  fprodmodd  11825  negdvdsb  11991  dvdsnegb  11992  dvdsmul1  11997  dvdsabseq  12031  dvdsssfz1  12036  odd2np1  12057  ndvdsadd  12115  dvdssqim  12218  nn0seqcvgd  12236  algcvgblem  12244  cncongr2  12299  prmind2  12315  prmdvdsfz  12334  prmndvdsfaclt  12351  dvdsfi  12434  modprm0  12450  modprmn0modprm0  12452  pythagtriplem1  12461  pythagtriplem4  12464  pythagtriplem8  12468  pythagtriplem9  12469  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem16  12475  pcexp  12505  pc2dvds  12526  pcz  12528  fldivp1  12544  pcfac  12546  oddprmdvds  12550  pockthg  12553  infpnlem1  12555  1arith  12563  4sqlem11  12597  pwsval  12995  ismgmid  13081  mhmpropd  13170  grpsubid1  13289  mulgnnp1  13338  mulgsubcl  13344  mulgnn0z  13357  mulgnndir  13359  mulgneg2  13364  ghmco  13472  gsumfzfsumlemm  14221  resttopon  14493  cnovex  14518  iscn  14519  iscnp  14521  cnco  14543  cndis  14563  hmeoco  14638  bl2in  14725  metss2lem  14819  metss2  14820  bdxmet  14823  metrest  14828  ioo2bl  14873  expcn  14891  elcncf  14895  dvexp  15033  plypow  15066  relogexp  15194  logcxp  15219  wilthlem1  15302  sgmnncl  15310  mpodvdsmulf1o  15312  lgsdirnn0  15374  gausslemma2dlem1a  15385  lgsquadlem1  15404  lgsquad2  15410  lgsquad3  15411  supfz  15806