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  1770  sseqtrid  3229  ssdifin0  3528  uneqdifeqim  3532  unimax  3869  opth  4266  djussxp  4807  iss  4988  relresfld  5195  eldmrexrn  5699  f1oresrab  5723  fmptco  5724  fsn  5730  fnressn  5744  foima2  5794  foeqcnvco  5833  isoini2  5862  ofres  6145  ofco  6149  tposexg  6311  tfrlemisucaccv  6378  tfrlemibex  6382  tfri1dALT  6404  tfrcl  6417  rdgivallem  6434  frecabex  6451  frectfr  6453  frecrdg  6461  pmresg  6730  mapsn  6744  mapsncnv  6749  ixpsnf1o  6790  en1  6853  2dom  6859  enpr2d  6871  mapxpen  6904  phplem4  6911  exmidpw2en  6968  fiintim  6985  sbthlem2  7017  elfir  7032  infglbti  7084  caseinl  7150  caseinr  7151  difinfsnlem  7158  difinfsn  7159  nninfisollemne  7190  exmidfodomrlemim  7261  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  2omotaplemap  7317  archnqq  7477  prarloclemlt  7553  prarloclemlo  7554  prarloclemcalc  7562  recexprlemm  7684  recexprlemex  7697  caucvgprlemm  7728  caucvgprprlemmu  7755  suplocexprlem2b  7774  suplocexprlemmu  7778  suplocexprlemlub  7784  1idsr  7828  recexgt0sr  7833  archsr  7842  caucvgsrlemoffval  7856  caucvgsrlemofff  7857  caucvgsrlemoffres  7860  caucvgsr  7862  ltpsrprg  7863  suplocsrlem  7868  pitonnlem2  7907  pitonn  7908  pitoregt0  7909  pitore  7910  recnnre  7911  axrnegex  7939  nntopi  7954  msqge0  8635  mulge0  8638  recexaplem2  8671  recexap  8672  recgt0  8869  recreclt  8919  nn1m1nn  9000  nn1suc  9001  nnle1eq1  9006  nn1gt1  9016  nnsub  9021  addltmul  9219  nn0le0eq0  9268  elnn0nn  9282  elnnz  9327  elznn0  9332  zlem1lt  9373  zltlem1  9374  elz2  9388  nn0n0n1ge2b  9396  nn0lt2  9398  nn0le2is012  9399  eluzaddi  9619  eluzsubi  9620  uzp1  9626  peano2uzr  9650  nn01to3  9682  qreccl  9707  irrmulap  9713  ltpnf  9846  xaddass2  9936  iccen  10072  fz01en  10119  fzpreddisj  10137  fzsuc2  10145  fseq1p1m1  10160  fseq1m1p1  10161  elfzp1b  10163  fzoss2  10239  fzval3  10271  fzosplitsnm1  10276  fzosplitprm1  10301  flhalf  10371  fldiv4lem1div2uz2  10375  modqmulnn  10413  modqmuladdnn0  10439  frec2uzrand  10476  frecuzrdg0  10484  frecuzrdg0t  10493  frecfzennn  10497  frecfzen2  10498  uzennn  10507  seqeq1  10521  seqp1g  10537  seqclg  10543  seq3m1  10544  monoord2  10557  ser3mono  10558  seqf1oglem1  10590  seqf1oglem2  10591  seqfeq4g  10602  ser0f  10605  exp3vallem  10611  expm1t  10638  expeq0  10641  expubnd  10667  binom3  10728  facndiv  10810  facavg  10817  bcn0  10826  bcnp1n  10830  bcm1k  10831  bcp1nk  10833  bcval5  10834  bcn2  10835  bcp1m1  10836  bcpasc  10837  bcn2m1  10840  hashsng  10869  hashun  10876  hashfz  10892  hashfzo  10893  seq3coll  10913  iswrdiz  10921  snopiswrd  10924  shftfval  10965  2shfti  10975  resqrexlemf1  11152  abs00ap  11206  sqabs  11226  ltabs  11231  caubnd2  11261  max0addsup  11363  rexico  11365  mulcn2  11455  climaddc1  11472  climmulc2  11474  climsubc1  11475  climsubc2  11476  iserex  11482  climlec2  11484  iser3shft  11489  climcvg1nlem  11492  serf0  11495  sumrbdc  11522  fsumm1  11559  fsump1  11563  fsum00  11605  telfsumo  11609  fsumparts  11613  hashiun  11621  binomlem  11626  binom1dif  11630  bcxmas  11632  isumsplit  11634  isum1p  11635  arisum  11641  arisum2  11642  trireciplem  11643  explecnv  11648  geolim  11654  georeclim  11656  mertenslem2  11679  mertensabs  11680  prodf1f  11686  prodrbdclem2  11716  efcllemp  11801  ef0lem  11803  efgt0  11827  eftlub  11833  efsep  11834  effsumlt  11835  tanval3ap  11857  efi4p  11860  resin4p  11861  recos4p  11862  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  sinltxirr  11904  sin01gt0  11905  cos01gt0  11906  absefib  11914  efieq1re  11915  eirraplem  11920  dvdsdc  11941  dvdscmulr  11963  dvdslelemd  11985  odd2np1lem  12013  odd2np1  12014  flodddiv4  12075  gcdsupex  12094  gcdsupcl  12095  gcd1  12124  nninfctlemfo  12177  nn0seqcvgd  12179  algcvg  12186  algcvgblem  12187  eucalg  12197  prmind2  12258  qden1elz  12343  dfphi2  12358  phiprm  12361  phimullem  12363  prmdiv  12373  prmdiveq  12374  prm23lt5  12401  pcpre1  12430  pczpre  12435  pcdiv  12440  pc1  12443  pcqdiv  12445  pcexp  12447  pcxnn0cl  12448  pcxcl  12449  pcdvdstr  12465  pc2dvds  12468  sumhashdc  12485  fldivp1  12486  pcfaclem  12487  qexpz  12490  expnprm  12491  prmpwdvds  12493  pockthlem  12494  4sqlem5  12520  4sqlem6  12521  4sqlem11  12539  4sqlem13m  12541  4sqlem19  12547  oddennn  12549  xpct  12553  ennnfonelemj0  12558  ennnfonelemen  12578  ctinfomlemom  12584  omctfn  12600  restid  12861  prdsex  12880  imasbas  12890  imasplusg  12891  imasmulr  12892  imasaddfnlemg  12897  xpscf  12930  igsumvalx  12972  gsumsplit1r  12981  gsumprval  12982  gsumfzz  13067  gsumfzcl  13071  mulgnngsum  13197  mulgnndir  13221  mulgneg2  13226  dvdsrmuld  13592  zsssubrg  14073  znval  14124  znle  14125  znbaslemnn  14127  znf1o  14139  znleval  14141  psrval  14152  restuni2  14345  cnrest2r  14405  lmfss  14412  lmres  14416  lmtopcnp  14418  ispsmet  14491  isxmet2d  14516  ismet2  14522  blfvalps  14553  blex  14555  xblss2  14573  reopnap  14706  divcnap  14723  climcncf  14739  cncfmpt2fcntop  14753  hovera  14801  limcdifap  14816  cnplimcim  14821  cnlimcim  14825  cnlimc  14826  cnlimci  14827  dvbss  14839  dvcnp2cntop  14848  dvcn  14849  dvaddxxbr  14850  dvmulxxbr  14851  dvexp  14860  dveflem  14872  plyval  14878  elply2  14881  plyf  14883  plyss  14884  plyssc  14885  elplyr  14886  plyaddlem1  14893  plymullem1  14894  plyaddlem  14895  plymullem  14896  reeff1olem  14906  sinperlem  14943  sin2kpi  14946  cos2kpi  14947  sin2pim  14948  cos2pim  14949  cosq14gt0  14967  coseq0q4123  14969  tangtx  14973  abssinper  14981  sinkpi  14982  coskpi  14983  cosq34lt1  14985  logrpap0b  15011  logdivlti  15016  rpcxpsqrtth  15064  rpabscxpbnd  15073  binom4  15111  wilthlem1  15112  lgslem1  15116  lgsval  15120  lgsfvalg  15121  lgsfcl2  15122  lgsfcl  15124  lgsval2lem  15126  lgsvalmod  15135  lgsneg  15140  lgsdilem  15143  lgsdir2lem3  15146  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgsabs1  15155  lgsprme0  15158  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem0d  15168  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem3  15179  gausslemma2dlem4  15180  gausslemma2dlem5a  15181  gausslemma2dlem5  15182  gausslemma2dlem6  15183  lgseisenlem2  15187  lgseisen  15190  lgsquadlem1  15191  m1lgs  15192  2sqlem9  15211  2sqlem10  15212  pwle2  15489  pw1nct  15493  nninfsellemdc  15500  nnnninfen  15511  sbthom  15516  trirec0  15534  apdifflemr  15537  reap0  15548  nconstwlpolem  15555