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  1807  sseqtrid  3278  ssdifin0  3578  uneqdifeqim  3582  unimax  3932  opth  4335  djussxp  4881  iss  5065  relresfld  5273  eldmrexrn  5796  f1oresrab  5820  fmptco  5821  fsn  5827  fnressn  5848  foima2  5902  foeqcnvco  5941  isoini2  5970  relmptopab  6234  ofres  6259  ofco  6263  suppval1  6417  suppimacnvfn  6424  tposexg  6467  tfrlemisucaccv  6534  tfrlemibex  6538  tfri1dALT  6560  tfrcl  6573  rdgivallem  6590  frecabex  6607  frectfr  6609  frecrdg  6617  pmresg  6888  mapsn  6902  mapsncnv  6907  ixpsnf1o  6948  en1  7016  2dom  7023  enpr2d  7040  en2  7041  mapxpen  7077  phplem4  7084  exmidpw2en  7147  fiintim  7166  sbthlem2  7200  elfir  7215  infglbti  7267  caseinl  7333  caseinr  7334  difinfsnlem  7341  difinfsn  7342  nninfisollemne  7373  exmidfodomrlemim  7455  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  2omotaplemap  7519  archnqq  7680  prarloclemlt  7756  prarloclemlo  7757  prarloclemcalc  7765  recexprlemm  7887  recexprlemex  7900  caucvgprlemm  7931  caucvgprprlemmu  7958  suplocexprlem2b  7977  suplocexprlemmu  7981  suplocexprlemlub  7987  1idsr  8031  recexgt0sr  8036  archsr  8045  caucvgsrlemoffval  8059  caucvgsrlemofff  8060  caucvgsrlemoffres  8063  caucvgsr  8065  ltpsrprg  8066  suplocsrlem  8071  pitonnlem2  8110  pitonn  8111  pitoregt0  8112  pitore  8113  recnnre  8114  axrnegex  8142  nntopi  8157  msqge0  8839  mulge0  8842  recexaplem2  8875  recexap  8876  recgt0  9073  recreclt  9123  nn1m1nn  9204  nn1suc  9205  nnle1eq1  9210  nn1gt1  9220  nnsub  9225  addltmul  9424  nn0le0eq0  9473  elnn0nn  9487  elnnz  9532  elznn0  9537  zlem1lt  9579  zltlem1  9580  elz2  9594  nn0n0n1ge2b  9602  nn0lt2  9604  nn0le2is012  9605  eluzaddi  9826  eluzsubi  9827  uzp1  9833  peano2uzr  9862  nn01to3  9894  qreccl  9919  irrmulap  9925  ltpnf  10058  xaddass2  10148  iccen  10284  fz01en  10331  fzpreddisj  10349  fzsuc2  10357  fseq1p1m1  10372  fseq1m1p1  10373  elfzp1b  10375  fzoss2  10452  fzval3  10493  fzosplitsnm1  10498  fzosplitprm1  10524  flhalf  10606  fldiv4lem1div2uz2  10610  modqmulnn  10648  modqmuladdnn0  10674  frec2uzrand  10711  frecuzrdg0  10719  frecuzrdg0t  10728  frecfzennn  10732  frecfzen2  10733  uzennn  10742  seqeq1  10756  seqp1g  10772  seqclg  10778  seq3m1  10779  monoord2  10792  ser3mono  10793  seqf1oglem1  10825  seqf1oglem2  10826  seqfeq4g  10837  ser0f  10840  exp3vallem  10846  expm1t  10873  expeq0  10876  expubnd  10902  binom3  10963  facndiv  11045  facavg  11052  bcn0  11061  bcnp1n  11065  bcm1k  11066  bcp1nk  11068  bcval5  11069  bcn2  11070  bcp1m1  11071  bcpasc  11072  bcn2m1  11075  hashsng  11104  hashun  11112  hashfz  11129  hashfzo  11130  seq3coll  11150  hash2en  11151  iswrdiz  11167  snopiswrd  11170  ccat1st1st  11265  swrds1  11296  cats1un  11349  wrdind  11350  wrd2ind  11351  swrdccatin1  11353  swrdccat3blem  11367  shftfval  11442  2shfti  11452  resqrexlemf1  11629  abs00ap  11683  sqabs  11703  ltabs  11708  caubnd2  11738  max0addsup  11840  rexico  11842  mulcn2  11933  climaddc1  11950  climmulc2  11952  climsubc1  11953  climsubc2  11954  iserex  11960  climlec2  11962  iser3shft  11967  climcvg1nlem  11970  serf0  11973  sumrbdc  12001  fsumm1  12038  fsump1  12042  fsum00  12084  telfsumo  12088  fsumparts  12092  hashiun  12100  binomlem  12105  binom1dif  12109  bcxmas  12111  isumsplit  12113  isum1p  12114  arisum  12120  arisum2  12121  trireciplem  12122  explecnv  12127  geolim  12133  georeclim  12135  mertenslem2  12158  mertensabs  12159  prodf1f  12165  prodrbdclem2  12195  efcllemp  12280  ef0lem  12282  efgt0  12306  eftlub  12312  efsep  12313  effsumlt  12314  tanval3ap  12336  efi4p  12339  resin4p  12340  recos4p  12341  ef01bndlem  12378  sin01bnd  12379  cos01bnd  12380  sinltxirr  12383  sin01gt0  12384  cos01gt0  12385  absefib  12393  efieq1re  12394  eirraplem  12399  dvdsdc  12420  dvdscmulr  12442  fsumdvds  12464  dvdslelemd  12465  3dvds  12486  odd2np1lem  12494  odd2np1  12495  flodddiv4  12558  bitsfzo  12577  bitsmod  12578  gcdsupex  12589  gcdsupcl  12590  gcd1  12619  nninfctlemfo  12672  nn0seqcvgd  12674  algcvg  12681  algcvgblem  12682  eucalg  12692  prmind2  12753  qden1elz  12838  dfphi2  12853  phiprm  12856  phimullem  12858  prmdiv  12868  prmdiveq  12869  prm23lt5  12897  pcpre1  12926  pczpre  12931  pcdiv  12936  pc1  12939  pcqdiv  12941  pcexp  12943  pcxnn0cl  12944  pcxcl  12945  pcdvdstr  12961  pc2dvds  12964  sumhashdc  12981  fldivp1  12982  pcfaclem  12983  qexpz  12986  expnprm  12987  prmpwdvds  12989  pockthlem  12990  4sqlem5  13016  4sqlem6  13017  4sqlem11  13035  4sqlem13m  13037  4sqlem19  13043  oddennn  13074  xpct  13078  ennnfonelemj0  13083  ennnfonelemen  13103  ctinfomlemom  13109  omctfn  13125  restid  13394  prdsex  13413  prdsval  13417  prdsbaslemss  13418  prdsbas  13420  imasbas  13451  imasplusg  13452  imasmulr  13453  imasaddfnlemg  13458  xpscf  13491  igsumvalx  13533  gsumsplit1r  13542  gsumprval  13543  gsumfzz  13639  gsumfzcl  13643  prdsgrpd  13753  prdsinvgd  13754  mulgnngsum  13775  mulgnndir  13799  mulgneg2  13804  dvdsrmuld  14172  zsssubrg  14661  znval  14712  znle  14713  znbaslemnn  14715  znf1o  14727  znleval  14729  psrval  14742  restuni2  14968  cnrest2r  15028  lmfss  15035  lmres  15039  lmtopcnp  15041  ispsmet  15114  isxmet2d  15139  ismet2  15145  blfvalps  15176  blex  15178  xblss2  15196  reopnap  15337  divcnap  15356  climcncf  15375  cncfmpt2fcntop  15390  hovera  15438  limcdifap  15453  cnplimcim  15458  cnlimcim  15462  cnlimc  15463  cnlimci  15464  dvbss  15476  dvcnp2cntop  15490  dvcn  15491  dvaddxxbr  15492  dvmulxxbr  15493  dvexp  15502  dveflem  15517  plyval  15523  elply2  15526  plyf  15528  plyss  15529  plyssc  15530  elplyr  15531  plyaddlem1  15538  plymullem1  15539  plyaddlem  15540  plymullem  15541  plyco  15550  plycj  15552  dvply1  15556  reeff1olem  15562  sinperlem  15599  sin2kpi  15602  cos2kpi  15603  sin2pim  15604  cos2pim  15605  cosq14gt0  15623  coseq0q4123  15625  tangtx  15629  abssinper  15637  sinkpi  15638  coskpi  15639  cosq34lt1  15641  logrpap0b  15667  logdivlti  15672  rpcxpsqrtth  15721  rpabscxpbnd  15731  binom4  15770  wilthlem1  15774  0sgm  15779  1sgmprm  15788  1sgm2ppw  15789  mersenne  15791  perfect1  15792  perfectlem1  15793  perfectlem2  15794  perfect  15795  lgslem1  15799  lgsval  15803  lgsfvalg  15804  lgsfcl2  15805  lgsfcl  15807  lgsval2lem  15809  lgsvalmod  15818  lgsneg  15823  lgsdilem  15826  lgsdir2lem3  15829  lgsdir  15834  lgsdilem2  15835  lgsdi  15836  lgsne0  15837  lgsabs1  15838  lgsprme0  15841  lgsdirnn0  15846  lgsdinn0  15847  gausslemma2dlem0d  15851  gausslemma2dlem1a  15857  gausslemma2dlem1f1o  15859  gausslemma2dlem3  15862  gausslemma2dlem4  15863  gausslemma2dlem5a  15864  gausslemma2dlem5  15865  gausslemma2dlem6  15866  lgseisenlem2  15870  lgseisen  15873  lgsquadlem1  15876  lgsquadlem2  15877  lgsquad2lem1  15880  lgsquad2lem2  15881  lgsquad2  15882  m1lgs  15884  2lgslem1  15890  2lgslem2  15891  2lgs  15903  2sqlem9  15923  2sqlem10  15924  ushgredgedg  16147  ushgredgedgloop  16149  uhgrspansubgrlem  16197  wlkvtxiedg  16266  wlkvtxiedgg  16267  wlk1walkdom  16280  upgr2wlkdc  16298  clwwlkccatlem  16321  umgrclwwlkge2  16323  clwwlknonmpo  16349  clwwlknonex2lem2  16359  clwwlknonex2  16360  konigsberglem1  16409  2omap  16695  pwle2  16700  pw1nct  16705  nninfsellemdc  16716  nnnninfen  16727  nnnninfex  16728  nninfnfiinf  16729  sbthom  16734  repiecelem  16737  repiecele0  16738  trirec0  16756  apdifflemr  16759  reap0  16771  nconstwlpolem  16778  gfsumval  16789