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  1808  sseqtrid  3292  ssdifin0  3596  uneqdifeqim  3600  unimax  3954  opth  4359  djussxp  4907  iss  5091  relresfld  5299  eldmrexrn  5825  f1oresrab  5849  fmptco  5850  fsn  5856  fnressn  5877  foima2  5932  foeqcnvco  5971  isoini2  6000  relmptopab  6266  ofres  6292  ofco  6296  suppval1  6454  suppimacnvfn  6461  tposexg  6504  tfrlemisucaccv  6571  tfrlemibex  6575  tfri1dALT  6597  tfrcl  6610  rdgivallem  6627  frecabex  6644  frectfr  6646  frecrdg  6654  pmresg  6925  mapsnd  6938  mapsn  6940  mapsncnv  6945  ixpsnf1o  6986  en1  7054  2dom  7061  mapsnend  7067  enpr2d  7079  en2  7080  mapxpen  7116  mapunen  7119  phplem4  7124  exmidpw2en  7187  fiintim  7206  sbthlem2  7243  elfir  7275  2omap  7284  infglbti  7331  caseinl  7397  caseinr  7398  difinfsnlem  7405  difinfsn  7406  nninfisollemne  7437  exmidfodomrlemim  7519  exmidfodomrlemr  7520  exmidfodomrlemrALT  7521  2omotaplemap  7589  archnqq  7750  prarloclemlt  7826  prarloclemlo  7827  prarloclemcalc  7835  recexprlemm  7957  recexprlemex  7970  caucvgprlemm  8001  caucvgprprlemmu  8028  suplocexprlem2b  8047  suplocexprlemmu  8051  suplocexprlemlub  8057  1idsr  8101  recexgt0sr  8106  archsr  8115  caucvgsrlemoffval  8129  caucvgsrlemofff  8130  caucvgsrlemoffres  8133  caucvgsr  8135  ltpsrprg  8136  suplocsrlem  8141  pitonnlem2  8180  pitonn  8181  pitoregt0  8182  pitore  8183  recnnre  8184  axrnegex  8212  nntopi  8227  msqge0  8910  mulge0  8913  recexaplem2  8946  recexap  8947  recgt0  9146  recreclt  9196  nn1m1nn  9277  nn1suc  9278  nnle1eq1  9283  nn1gt1  9293  nnsub  9298  addltmul  9497  nn0le0eq0  9546  elnn0nn  9560  elnnz  9609  elznn0  9614  zlem1lt  9656  zltlem1  9657  elz2  9671  nn0n0n1ge2b  9680  nn0lt2  9682  nn0le2is012  9683  eluzaddi  9904  eluzsubi  9905  uzp1  9911  peano2uzr  9940  nn01to3  9972  qreccl  9997  irrmulap  10003  ltpnf  10137  xaddass2  10227  iccen  10364  fz01en  10413  fzpreddisj  10432  fzsuc2  10440  fseq1p1m1  10455  fseq1m1p1  10456  elfzp1b  10458  fzoss2  10535  fzval3  10576  fzosplitsnm1  10581  fzosplitprm1  10607  flhalf  10691  fldiv4lem1div2uz2  10695  modqmulnn  10733  modqmuladdnn0  10759  frec2uzrand  10796  frecuzrdg0  10804  frecuzrdg0t  10813  frecfzennn  10817  frecfzen2  10818  uzennn  10827  seqeq1  10841  seqp1g  10857  seqclg  10863  seq3m1  10864  monoord2  10877  ser3mono  10878  seqf1oglem1  10910  seqf1oglem2  10911  seqfeq4g  10922  ser0f  10925  exp3vallem  10931  expm1t  10958  expeq0  10961  expubnd  10987  binom3  11048  facndiv  11131  facavg  11138  bcn0  11147  bcnp1n  11151  bcm1k  11152  bcp1nk  11154  bcval5  11155  bcn2  11156  bcp1m1  11157  bcpasc  11158  bcn2m1  11162  hashsng  11191  hashun  11199  hashfz  11216  hashfzo  11217  hashmap  11222  hashfibclem  11236  seq3coll  11244  hash2en  11245  iswrdiz  11261  snopiswrd  11264  ccat1st1st  11359  swrds1  11390  cats1un  11443  wrdind  11444  wrd2ind  11445  swrdccatin1  11447  swrdccat3blem  11461  shftfval  11536  2shfti  11546  resqrexlemf1  11724  abs00ap  11778  sqabs  11798  ltabs  11803  caubnd2  11833  max0addsup  11935  rexico  11937  mulcn2  12028  climaddc1  12045  climmulc2  12047  climsubc1  12048  climsubc2  12049  iserex  12055  climlec2  12057  iser3shft  12062  climcvg1nlem  12065  serf0  12068  sumrbdc  12096  fsumm1  12133  fsump1  12137  fsum00  12179  telfsumo  12183  fsumparts  12187  hashiun  12195  binomlem  12200  binom1dif  12204  bcxmas  12206  isumsplit  12208  isum1p  12209  arisum  12215  arisum2  12216  trireciplem  12217  explecnv  12222  geolim  12228  georeclim  12230  mertenslem2  12253  mertensabs  12254  prodf1f  12260  prodrbdclem2  12290  efcllemp  12375  ef0lem  12377  efgt0  12401  eftlub  12407  efsep  12408  effsumlt  12409  tanval3ap  12431  efi4p  12434  resin4p  12435  recos4p  12436  ef01bndlem  12473  sin01bnd  12474  cos01bnd  12475  sinltxirr  12478  sin01gt0  12479  cos01gt0  12480  absefib  12488  efieq1re  12489  eirraplem  12494  dvdsdc  12515  dvdscmulr  12537  fsumdvds  12559  dvdslelemd  12560  3dvds  12581  odd2np1lem  12589  odd2np1  12590  flodddiv4  12653  bitsfzo  12672  bitsmod  12673  gcdsupex  12684  gcdsupcl  12685  gcd1  12714  nninfctlemfo  12767  nn0seqcvgd  12769  algcvg  12776  algcvgblem  12777  eucalg  12787  prmind2  12848  qden1elz  12933  dfphi2  12948  phiprm  12951  phimullem  12953  prmdiv  12963  prmdiveq  12964  prm23lt5  12992  pcpre1  13021  pczpre  13026  pcdiv  13031  pc1  13034  pcqdiv  13036  pcexp  13038  pcxnn0cl  13039  pcxcl  13040  pcdvdstr  13056  pc2dvds  13059  sumhashdc  13076  fldivp1  13077  pcfaclem  13078  qexpz  13081  expnprm  13082  prmpwdvds  13084  pockthlem  13085  4sqlem5  13111  4sqlem6  13112  4sqlem11  13130  4sqlem13m  13132  4sqlem19  13138  ballotfilemofi  13169  ballotfilemfc0  13182  ballotfilemfcc  13183  ballotfilemodife  13190  ballotfilemscl  13197  ballotfilemsle  13198  oddennn  13233  xpct  13237  ennnfonelemj0  13242  ennnfonelemen  13262  ctinfomlemom  13268  omctfn  13284  restid  13553  imasbas  13577  imasplusg  13578  imasmulr  13579  imasaddfnlemg  13584  xpscf  13617  igsumvalx  13658  gsumsplit1r  13667  gsumprval  13668  gsumfzz  13756  gsumfzcl  13760  mulgnngsum  13886  mulgnndir  13910  mulgneg2  13915  gfsumval  14108  prdsex  14120  prdsval  14121  prdsbaslemss  14122  prdsbas  14124  prdsgrpd  14145  prdsinvgd  14146  dvdsrmuld  14347  zsssubrg  14865  znval  14916  znle  14917  znbaslemnn  14919  znf1o  14931  znleval  14933  psrval  14946  restuni2  15174  cnrest2r  15234  lmfss  15241  lmres  15245  lmtopcnp  15247  ispsmet  15320  isxmet2d  15345  ismet2  15351  blfvalps  15382  blex  15384  xblss2  15402  reopnap  15543  divcnap  15562  climcncf  15581  cncfmpt2fcntop  15596  hovera  15644  limcdifap  15659  cnplimcim  15664  cnlimcim  15668  cnlimc  15669  cnlimci  15670  dvbss  15682  dvcnp2cntop  15696  dvcn  15697  dvaddxxbr  15698  dvmulxxbr  15699  dvexp  15708  dveflem  15723  plyval  15729  elply2  15732  plyf  15734  plyss  15735  plyssc  15736  elplyr  15737  plyaddlem1  15744  plymullem1  15745  plyaddlem  15746  plymullem  15747  plyco  15756  plycj  15758  dvply1  15762  reeff1olem  15768  sinperlem  15805  sin2kpi  15808  cos2kpi  15809  sin2pim  15810  cos2pim  15811  cosq14gt0  15829  coseq0q4123  15831  tangtx  15835  abssinper  15843  sinkpi  15844  coskpi  15845  cosq34lt1  15847  logrpap0b  15873  logdivlti  15878  rpcxpsqrtth  15927  rpabscxpbnd  15937  binom4  15976  wilthlem1  15980  0sgm  15985  1sgmprm  15994  1sgm2ppw  15995  mersenne  15997  perfect1  15998  perfectlem1  15999  perfectlem2  16000  perfect  16001  lgslem1  16005  lgsval  16009  lgsfvalg  16010  lgsfcl2  16011  lgsfcl  16013  lgsval2lem  16015  lgsvalmod  16024  lgsneg  16029  lgsdilem  16032  lgsdir2lem3  16035  lgsdir  16040  lgsdilem2  16041  lgsdi  16042  lgsne0  16043  lgsabs1  16044  lgsprme0  16047  lgsdirnn0  16052  lgsdinn0  16053  gausslemma2dlem0d  16057  gausslemma2dlem1a  16063  gausslemma2dlem1f1o  16065  gausslemma2dlem3  16068  gausslemma2dlem4  16069  gausslemma2dlem5a  16070  gausslemma2dlem5  16071  gausslemma2dlem6  16072  lgseisenlem2  16076  lgseisen  16079  lgsquadlem1  16082  lgsquadlem2  16083  lgsquad2lem1  16086  lgsquad2lem2  16087  lgsquad2  16088  m1lgs  16090  2lgslem1  16096  2lgslem2  16097  2lgs  16109  2sqlem9  16129  2sqlem10  16130  ushgredgedg  16353  ushgredgedgloop  16355  uhgrspansubgrlem  16403  wlkvtxiedg  16472  wlkvtxiedgg  16473  wlk1walkdom  16486  upgr2wlkdc  16504  clwwlkccatlem  16527  umgrclwwlkge2  16529  clwwlknonmpo  16555  clwwlknonex2lem2  16565  clwwlknonex2  16566  konigsberglem1  16615  pwle2  16914  pw1nct  16919  nninfsellemdc  16930  nnnninfen  16941  nnnninfex  16942  nninfnfiinf  16943  sbthom  16948  repiecelem  16951  repiecele0  16952  trirec0  16970  apdifflemr  16973  reap0  16985  nconstwlpolem  16992