Theorem sylancl 413

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancl.1	⊢ (𝜑 → 𝜓)
sylancl.2	⊢ 𝜒
sylancl.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylancl	⊢ (𝜑 → 𝜃)

Proof of Theorem sylancl

Step	Hyp	Ref	Expression
1		sylancl.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylancl.2	. . 3 ⊢ 𝜒
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝜒)
4		sylancl.3	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 3, 4	syl2anc 411	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  sylanblc  415  sylanblrc  416  equveli  1805  sseqtrid  3274  ssdifin0  3573  uneqdifeqim  3577  unimax  3922  opth  4323  djussxp  4867  iss  5051  relresfld  5258  eldmrexrn  5778  f1oresrab  5802  fmptco  5803  fsn  5809  fnressn  5829  foima2  5881  foeqcnvco  5920  isoini2  5949  relmptopab  6213  ofres  6239  ofco  6243  tposexg  6410  tfrlemisucaccv  6477  tfrlemibex  6481  tfri1dALT  6503  tfrcl  6516  rdgivallem  6533  frecabex  6550  frectfr  6552  frecrdg  6560  pmresg  6831  mapsn  6845  mapsncnv  6850  ixpsnf1o  6891  en1  6959  2dom  6966  enpr2d  6980  en2  6981  mapxpen  7017  phplem4  7024  exmidpw2en  7082  fiintim  7101  sbthlem2  7133  elfir  7148  infglbti  7200  caseinl  7266  caseinr  7267  difinfsnlem  7274  difinfsn  7275  nninfisollemne  7306  exmidfodomrlemim  7387  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  2omotaplemap  7451  archnqq  7612  prarloclemlt  7688  prarloclemlo  7689  prarloclemcalc  7697  recexprlemm  7819  recexprlemex  7832  caucvgprlemm  7863  caucvgprprlemmu  7890  suplocexprlem2b  7909  suplocexprlemmu  7913  suplocexprlemlub  7919  1idsr  7963  recexgt0sr  7968  archsr  7977  caucvgsrlemoffval  7991  caucvgsrlemofff  7992  caucvgsrlemoffres  7995  caucvgsr  7997  ltpsrprg  7998  suplocsrlem  8003  pitonnlem2  8042  pitonn  8043  pitoregt0  8044  pitore  8045  recnnre  8046  axrnegex  8074  nntopi  8089  msqge0  8771  mulge0  8774  recexaplem2  8807  recexap  8808  recgt0  9005  recreclt  9055  nn1m1nn  9136  nn1suc  9137  nnle1eq1  9142  nn1gt1  9152  nnsub  9157  addltmul  9356  nn0le0eq0  9405  elnn0nn  9419  elnnz  9464  elznn0  9469  zlem1lt  9511  zltlem1  9512  elz2  9526  nn0n0n1ge2b  9534  nn0lt2  9536  nn0le2is012  9537  eluzaddi  9757  eluzsubi  9758  uzp1  9764  peano2uzr  9788  nn01to3  9820  qreccl  9845  irrmulap  9851  ltpnf  9984  xaddass2  10074  iccen  10210  fz01en  10257  fzpreddisj  10275  fzsuc2  10283  fseq1p1m1  10298  fseq1m1p1  10299  elfzp1b  10301  fzoss2  10378  fzval3  10418  fzosplitsnm1  10423  fzosplitprm1  10448  flhalf  10530  fldiv4lem1div2uz2  10534  modqmulnn  10572  modqmuladdnn0  10598  frec2uzrand  10635  frecuzrdg0  10643  frecuzrdg0t  10652  frecfzennn  10656  frecfzen2  10657  uzennn  10666  seqeq1  10680  seqp1g  10696  seqclg  10702  seq3m1  10703  monoord2  10716  ser3mono  10717  seqf1oglem1  10749  seqf1oglem2  10750  seqfeq4g  10761  ser0f  10764  exp3vallem  10770  expm1t  10797  expeq0  10800  expubnd  10826  binom3  10887  facndiv  10969  facavg  10976  bcn0  10985  bcnp1n  10989  bcm1k  10990  bcp1nk  10992  bcval5  10993  bcn2  10994  bcp1m1  10995  bcpasc  10996  bcn2m1  10999  hashsng  11028  hashun  11035  hashfz  11051  hashfzo  11052  seq3coll  11072  hash2en  11073  iswrdiz  11086  snopiswrd  11089  ccat1st1st  11180  swrds1  11208  cats1un  11261  wrdind  11262  wrd2ind  11263  swrdccatin1  11265  swrdccat3blem  11279  shftfval  11340  2shfti  11350  resqrexlemf1  11527  abs00ap  11581  sqabs  11601  ltabs  11606  caubnd2  11636  max0addsup  11738  rexico  11740  mulcn2  11831  climaddc1  11848  climmulc2  11850  climsubc1  11851  climsubc2  11852  iserex  11858  climlec2  11860  iser3shft  11865  climcvg1nlem  11868  serf0  11871  sumrbdc  11898  fsumm1  11935  fsump1  11939  fsum00  11981  telfsumo  11985  fsumparts  11989  hashiun  11997  binomlem  12002  binom1dif  12006  bcxmas  12008  isumsplit  12010  isum1p  12011  arisum  12017  arisum2  12018  trireciplem  12019  explecnv  12024  geolim  12030  georeclim  12032  mertenslem2  12055  mertensabs  12056  prodf1f  12062  prodrbdclem2  12092  efcllemp  12177  ef0lem  12179  efgt0  12203  eftlub  12209  efsep  12210  effsumlt  12211  tanval3ap  12233  efi4p  12236  resin4p  12237  recos4p  12238  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  sinltxirr  12280  sin01gt0  12281  cos01gt0  12282  absefib  12290  efieq1re  12291  eirraplem  12296  dvdsdc  12317  dvdscmulr  12339  fsumdvds  12361  dvdslelemd  12362  3dvds  12383  odd2np1lem  12391  odd2np1  12392  flodddiv4  12455  bitsfzo  12474  bitsmod  12475  gcdsupex  12486  gcdsupcl  12487  gcd1  12516  nninfctlemfo  12569  nn0seqcvgd  12571  algcvg  12578  algcvgblem  12579  eucalg  12589  prmind2  12650  qden1elz  12735  dfphi2  12750  phiprm  12753  phimullem  12755  prmdiv  12765  prmdiveq  12766  prm23lt5  12794  pcpre1  12823  pczpre  12828  pcdiv  12833  pc1  12836  pcqdiv  12838  pcexp  12840  pcxnn0cl  12841  pcxcl  12842  pcdvdstr  12858  pc2dvds  12861  sumhashdc  12878  fldivp1  12879  pcfaclem  12880  qexpz  12883  expnprm  12884  prmpwdvds  12886  pockthlem  12887  4sqlem5  12913  4sqlem6  12914  4sqlem11  12932  4sqlem13m  12934  4sqlem19  12940  oddennn  12971  xpct  12975  ennnfonelemj0  12980  ennnfonelemen  13000  ctinfomlemom  13006  omctfn  13022  restid  13291  prdsex  13310  prdsval  13314  prdsbaslemss  13315  prdsbas  13317  imasbas  13348  imasplusg  13349  imasmulr  13350  imasaddfnlemg  13355  xpscf  13388  igsumvalx  13430  gsumsplit1r  13439  gsumprval  13440  gsumfzz  13536  gsumfzcl  13540  prdsgrpd  13650  prdsinvgd  13651  mulgnngsum  13672  mulgnndir  13696  mulgneg2  13701  dvdsrmuld  14068  zsssubrg  14557  znval  14608  znle  14609  znbaslemnn  14611  znf1o  14623  znleval  14625  psrval  14638  restuni2  14859  cnrest2r  14919  lmfss  14926  lmres  14930  lmtopcnp  14932  ispsmet  15005  isxmet2d  15030  ismet2  15036  blfvalps  15067  blex  15069  xblss2  15087  reopnap  15228  divcnap  15247  climcncf  15266  cncfmpt2fcntop  15281  hovera  15329  limcdifap  15344  cnplimcim  15349  cnlimcim  15353  cnlimc  15354  cnlimci  15355  dvbss  15367  dvcnp2cntop  15381  dvcn  15382  dvaddxxbr  15383  dvmulxxbr  15384  dvexp  15393  dveflem  15408  plyval  15414  elply2  15417  plyf  15419  plyss  15420  plyssc  15421  elplyr  15422  plyaddlem1  15429  plymullem1  15430  plyaddlem  15431  plymullem  15432  plyco  15441  plycj  15443  dvply1  15447  reeff1olem  15453  sinperlem  15490  sin2kpi  15493  cos2kpi  15494  sin2pim  15495  cos2pim  15496  cosq14gt0  15514  coseq0q4123  15516  tangtx  15520  abssinper  15528  sinkpi  15529  coskpi  15530  cosq34lt1  15532  logrpap0b  15558  logdivlti  15563  rpcxpsqrtth  15612  rpabscxpbnd  15622  binom4  15661  wilthlem1  15662  0sgm  15667  1sgmprm  15676  1sgm2ppw  15677  mersenne  15679  perfect1  15680  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgslem1  15687  lgsval  15691  lgsfvalg  15692  lgsfcl2  15693  lgsfcl  15695  lgsval2lem  15697  lgsvalmod  15706  lgsneg  15711  lgsdilem  15714  lgsdir2lem3  15717  lgsdir  15722  lgsdilem2  15723  lgsdi  15724  lgsne0  15725  lgsabs1  15726  lgsprme0  15729  lgsdirnn0  15734  lgsdinn0  15735  gausslemma2dlem0d  15739  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  gausslemma2dlem3  15750  gausslemma2dlem4  15751  gausslemma2dlem5a  15752  gausslemma2dlem5  15753  gausslemma2dlem6  15754  lgseisenlem2  15758  lgseisen  15761  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem1  15768  lgsquad2lem2  15769  lgsquad2  15770  m1lgs  15772  2lgslem1  15778  2lgslem2  15779  2lgs  15791  2sqlem9  15811  2sqlem10  15812  ushgredgedg  16032  ushgredgedgloop  16034  wlkvtxiedg  16066  wlkvtxiedgg  16067  wlk1walkdom  16080  upgr2wlkdc  16096  2omap  16388  pwle2  16393  pw1nct  16398  nninfsellemdc  16406  nnnninfen  16417  nnnninfex  16418  nninfnfiinf  16419  sbthom  16424  trirec0  16442  apdifflemr  16445  reap0  16456  nconstwlpolem  16463