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  3287  ssdifin0  3590  uneqdifeqim  3594  unimax  3947  opth  4352  djussxp  4899  iss  5083  relresfld  5291  eldmrexrn  5817  f1oresrab  5841  fmptco  5842  fsn  5848  fnressn  5869  foima2  5923  foeqcnvco  5962  isoini2  5991  relmptopab  6255  ofres  6280  ofco  6284  suppval1  6438  suppimacnvfn  6445  tposexg  6488  tfrlemisucaccv  6555  tfrlemibex  6559  tfri1dALT  6581  tfrcl  6594  rdgivallem  6611  frecabex  6628  frectfr  6630  frecrdg  6638  pmresg  6909  mapsnd  6922  mapsn  6924  mapsncnv  6929  ixpsnf1o  6970  en1  7038  2dom  7045  mapsnend  7051  enpr2d  7063  en2  7064  mapxpen  7100  mapunen  7103  phplem4  7108  exmidpw2en  7171  fiintim  7190  sbthlem2  7227  elfir  7259  2omap  7268  infglbti  7315  caseinl  7381  caseinr  7382  difinfsnlem  7389  difinfsn  7390  nninfisollemne  7421  exmidfodomrlemim  7503  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  2omotaplemap  7570  archnqq  7731  prarloclemlt  7807  prarloclemlo  7808  prarloclemcalc  7816  recexprlemm  7938  recexprlemex  7951  caucvgprlemm  7982  caucvgprprlemmu  8009  suplocexprlem2b  8028  suplocexprlemmu  8032  suplocexprlemlub  8038  1idsr  8082  recexgt0sr  8087  archsr  8096  caucvgsrlemoffval  8110  caucvgsrlemofff  8111  caucvgsrlemoffres  8114  caucvgsr  8116  ltpsrprg  8117  suplocsrlem  8122  pitonnlem2  8161  pitonn  8162  pitoregt0  8163  pitore  8164  recnnre  8165  axrnegex  8193  nntopi  8208  msqge0  8889  mulge0  8892  recexaplem2  8925  recexap  8926  recgt0  9123  recreclt  9173  nn1m1nn  9254  nn1suc  9255  nnle1eq1  9260  nn1gt1  9270  nnsub  9275  addltmul  9474  nn0le0eq0  9523  elnn0nn  9537  elnnz  9586  elznn0  9591  zlem1lt  9633  zltlem1  9634  elz2  9648  nn0n0n1ge2b  9656  nn0lt2  9658  nn0le2is012  9659  eluzaddi  9880  eluzsubi  9881  uzp1  9887  peano2uzr  9916  nn01to3  9948  qreccl  9973  irrmulap  9979  ltpnf  10112  xaddass2  10202  iccen  10339  fz01en  10386  fzpreddisj  10404  fzsuc2  10412  fseq1p1m1  10427  fseq1m1p1  10428  elfzp1b  10430  fzoss2  10507  fzval3  10548  fzosplitsnm1  10553  fzosplitprm1  10579  flhalf  10661  fldiv4lem1div2uz2  10665  modqmulnn  10703  modqmuladdnn0  10729  frec2uzrand  10766  frecuzrdg0  10774  frecuzrdg0t  10783  frecfzennn  10787  frecfzen2  10788  uzennn  10797  seqeq1  10811  seqp1g  10827  seqclg  10833  seq3m1  10834  monoord2  10847  ser3mono  10848  seqf1oglem1  10880  seqf1oglem2  10881  seqfeq4g  10892  ser0f  10895  exp3vallem  10901  expm1t  10928  expeq0  10931  expubnd  10957  binom3  11018  facndiv  11100  facavg  11107  bcn0  11116  bcnp1n  11120  bcm1k  11121  bcp1nk  11123  bcval5  11124  bcn2  11125  bcp1m1  11126  bcpasc  11127  bcn2m1  11130  hashsng  11159  hashun  11167  hashfz  11184  hashfzo  11185  hashfibclem  11202  seq3coll  11210  hash2en  11211  iswrdiz  11227  snopiswrd  11230  ccat1st1st  11325  swrds1  11356  cats1un  11409  wrdind  11410  wrd2ind  11411  swrdccatin1  11413  swrdccat3blem  11427  shftfval  11502  2shfti  11512  resqrexlemf1  11689  abs00ap  11743  sqabs  11763  ltabs  11768  caubnd2  11798  max0addsup  11900  rexico  11902  mulcn2  11993  climaddc1  12010  climmulc2  12012  climsubc1  12013  climsubc2  12014  iserex  12020  climlec2  12022  iser3shft  12027  climcvg1nlem  12030  serf0  12033  sumrbdc  12061  fsumm1  12098  fsump1  12102  fsum00  12144  telfsumo  12148  fsumparts  12152  hashiun  12160  binomlem  12165  binom1dif  12169  bcxmas  12171  isumsplit  12173  isum1p  12174  arisum  12180  arisum2  12181  trireciplem  12182  explecnv  12187  geolim  12193  georeclim  12195  mertenslem2  12218  mertensabs  12219  prodf1f  12225  prodrbdclem2  12255  efcllemp  12340  ef0lem  12342  efgt0  12366  eftlub  12372  efsep  12373  effsumlt  12374  tanval3ap  12396  efi4p  12399  resin4p  12400  recos4p  12401  ef01bndlem  12438  sin01bnd  12439  cos01bnd  12440  sinltxirr  12443  sin01gt0  12444  cos01gt0  12445  absefib  12453  efieq1re  12454  eirraplem  12459  dvdsdc  12480  dvdscmulr  12502  fsumdvds  12524  dvdslelemd  12525  3dvds  12546  odd2np1lem  12554  odd2np1  12555  flodddiv4  12618  bitsfzo  12637  bitsmod  12638  gcdsupex  12649  gcdsupcl  12650  gcd1  12679  nninfctlemfo  12732  nn0seqcvgd  12734  algcvg  12741  algcvgblem  12742  eucalg  12752  prmind2  12813  qden1elz  12898  dfphi2  12913  phiprm  12916  phimullem  12918  prmdiv  12928  prmdiveq  12929  prm23lt5  12957  pcpre1  12986  pczpre  12991  pcdiv  12996  pc1  12999  pcqdiv  13001  pcexp  13003  pcxnn0cl  13004  pcxcl  13005  pcdvdstr  13021  pc2dvds  13024  sumhashdc  13041  fldivp1  13042  pcfaclem  13043  qexpz  13046  expnprm  13047  prmpwdvds  13049  pockthlem  13050  4sqlem5  13076  4sqlem6  13077  4sqlem11  13095  4sqlem13m  13097  4sqlem19  13103  ballotfilemofi  13134  oddennn  13135  xpct  13139  ennnfonelemj0  13144  ennnfonelemen  13164  ctinfomlemom  13170  omctfn  13186  restid  13455  prdsex  13474  prdsval  13478  prdsbaslemss  13479  prdsbas  13481  imasbas  13512  imasplusg  13513  imasmulr  13514  imasaddfnlemg  13519  xpscf  13552  igsumvalx  13594  gsumsplit1r  13603  gsumprval  13604  gsumfzz  13700  gsumfzcl  13704  prdsgrpd  13814  prdsinvgd  13815  mulgnngsum  13836  mulgnndir  13860  mulgneg2  13865  dvdsrmuld  14233  zsssubrg  14725  znval  14776  znle  14777  znbaslemnn  14779  znf1o  14791  znleval  14793  psrval  14806  restuni2  15034  cnrest2r  15094  lmfss  15101  lmres  15105  lmtopcnp  15107  ispsmet  15180  isxmet2d  15205  ismet2  15211  blfvalps  15242  blex  15244  xblss2  15262  reopnap  15403  divcnap  15422  climcncf  15441  cncfmpt2fcntop  15456  hovera  15504  limcdifap  15519  cnplimcim  15524  cnlimcim  15528  cnlimc  15529  cnlimci  15530  dvbss  15542  dvcnp2cntop  15556  dvcn  15557  dvaddxxbr  15558  dvmulxxbr  15559  dvexp  15568  dveflem  15583  plyval  15589  elply2  15592  plyf  15594  plyss  15595  plyssc  15596  elplyr  15597  plyaddlem1  15604  plymullem1  15605  plyaddlem  15606  plymullem  15607  plyco  15616  plycj  15618  dvply1  15622  reeff1olem  15628  sinperlem  15665  sin2kpi  15668  cos2kpi  15669  sin2pim  15670  cos2pim  15671  cosq14gt0  15689  coseq0q4123  15691  tangtx  15695  abssinper  15703  sinkpi  15704  coskpi  15705  cosq34lt1  15707  logrpap0b  15733  logdivlti  15738  rpcxpsqrtth  15787  rpabscxpbnd  15797  binom4  15836  wilthlem1  15840  0sgm  15845  1sgmprm  15854  1sgm2ppw  15855  mersenne  15857  perfect1  15858  perfectlem1  15859  perfectlem2  15860  perfect  15861  lgslem1  15865  lgsval  15869  lgsfvalg  15870  lgsfcl2  15871  lgsfcl  15873  lgsval2lem  15875  lgsvalmod  15884  lgsneg  15889  lgsdilem  15892  lgsdir2lem3  15895  lgsdir  15900  lgsdilem2  15901  lgsdi  15902  lgsne0  15903  lgsabs1  15904  lgsprme0  15907  lgsdirnn0  15912  lgsdinn0  15913  gausslemma2dlem0d  15917  gausslemma2dlem1a  15923  gausslemma2dlem1f1o  15925  gausslemma2dlem3  15928  gausslemma2dlem4  15929  gausslemma2dlem5a  15930  gausslemma2dlem5  15931  gausslemma2dlem6  15932  lgseisenlem2  15936  lgseisen  15939  lgsquadlem1  15942  lgsquadlem2  15943  lgsquad2lem1  15946  lgsquad2lem2  15947  lgsquad2  15948  m1lgs  15950  2lgslem1  15956  2lgslem2  15957  2lgs  15969  2sqlem9  15989  2sqlem10  15990  ushgredgedg  16213  ushgredgedgloop  16215  uhgrspansubgrlem  16263  wlkvtxiedg  16332  wlkvtxiedgg  16333  wlk1walkdom  16346  upgr2wlkdc  16364  clwwlkccatlem  16387  umgrclwwlkge2  16389  clwwlknonmpo  16415  clwwlknonex2lem2  16425  clwwlknonex2  16426  konigsberglem1  16475  pwle2  16764  pw1nct  16769  nninfsellemdc  16780  nnnninfen  16791  nnnninfex  16792  nninfnfiinf  16793  sbthom  16798  repiecelem  16801  repiecele0  16802  trirec0  16820  apdifflemr  16823  reap0  16835  nconstwlpolem  16842  gfsumval  16853