Theorem sylancl 417

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 415	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  sylanblc  419  sylanblrc  420  equveli  1812  sseqtrid  3298  ssdifin0  3609  uneqdifeqim  3613  unimax  3969  opth  4377  djussxp  4925  iss  5109  relresfld  5317  eldmrexrn  5849  f1oresrab  5873  fmptco  5874  fsn  5880  fnressn  5901  foima2  5957  foeqcnvco  5996  isoini2  6025  relmptopab  6291  ofres  6317  ofco  6321  suppval1  6479  suppimacnvfn  6486  tposexg  6529  tfrlemisucaccv  6596  tfrlemibex  6600  tfri1dALT  6622  tfrcl  6635  rdgivallem  6652  frecabex  6669  frectfr  6671  frecrdg  6679  pmresg  6957  mapsnd  6970  mapsn  6972  mapsncnv  6977  ixpsnf1o  7018  en1  7086  2dom  7093  mapsnend  7099  enpr2d  7111  en2  7112  mapxpen  7148  mapunen  7151  phplem4  7156  exmidpw2en  7219  fiintim  7238  sbthlem2  7275  elfir  7307  2omap  7318  infglbti  7365  caseinl  7431  caseinr  7432  difinfsnlem  7439  difinfsn  7440  nninfisollemne  7471  exmidfodomrlemim  7553  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  2omotaplemap  7623  archnqq  7784  prarloclemlt  7860  prarloclemlo  7861  prarloclemcalc  7869  recexprlemm  7991  recexprlemex  8004  caucvgprlemm  8035  caucvgprprlemmu  8062  suplocexprlem2b  8081  suplocexprlemmu  8085  suplocexprlemlub  8091  1idsr  8135  recexgt0sr  8140  archsr  8149  caucvgsrlemoffval  8163  caucvgsrlemofff  8164  caucvgsrlemoffres  8167  caucvgsr  8169  ltpsrprg  8170  suplocsrlem  8175  pitonnlem2  8214  pitonn  8215  pitoregt0  8216  pitore  8217  recnnre  8218  axrnegex  8246  nntopi  8261  msqge0  8945  mulge0  8948  recexaplem2  8981  recexap  8982  recgt0  9181  recreclt  9231  nn1m1nn  9323  nn1suc  9324  nnle1eq1  9329  nn1gt1  9339  nnsub  9344  addltmul  9544  nn0le0eq0  9593  elnn0nn  9607  elnnz  9656  elznn0  9661  zlem1lt  9703  zltlem1  9704  elz2  9718  nn0n0n1ge2b  9727  nn0lt2  9729  nn0le2is012  9730  eluzaddi  9951  eluzsubi  9952  uzp1  9958  peano2uzr  9987  nn01to3  10019  qreccl  10044  irrmulap  10050  ltpnf  10184  xaddass2  10274  iccen  10411  fz01en  10461  fzpreddisj  10480  fzsuc2  10488  fseq1p1m1  10503  fseq1m1p1  10504  elfzp1b  10506  fzoss2  10583  fzval3  10624  fzosplitsnm1  10629  fzosplitprm1  10655  flhalf  10739  fldiv4lem1div2uz2  10743  modqmulnn  10781  modqmuladdnn0  10807  frec2uzrand  10844  frecuzrdg0  10852  frecuzrdg0t  10861  frecfzennn  10865  frecfzen2  10866  uzennn  10875  seqeq1  10889  seqp1g  10905  seqclg  10911  seq3m1  10912  monoord2  10925  ser3mono  10926  seqf1oglem1  10958  seqf1oglem2  10959  seqfeq4g  10970  ser0f  10973  exp3vallem  10979  expm1t  11006  expeq0  11009  expubnd  11035  binom3  11096  facndiv  11179  facavg  11186  bcn0  11195  bcnp1n  11199  bcm1k  11200  bcp1nk  11202  bcval5  11203  bcn2  11204  bcp1m1  11205  bcpasc  11206  bcn2m1  11210  hashsng  11239  hashun  11247  hashfz  11264  hashfzo  11265  hashmap  11270  hashfibclem  11284  hashf1lem1  11287  hashf1  11289  seq3coll  11296  hash2en  11297  iswrdiz  11313  snopiswrd  11316  ccat1st1st  11411  swrds1  11442  cats1un  11495  wrdind  11496  wrd2ind  11497  swrdccatin1  11499  swrdccat3blem  11513  shftfval  11588  2shfti  11598  resqrexlemf1  11776  abs00ap  11830  sqabs  11850  ltabs  11855  caubnd2  11885  max0addsup  11987  rexico  11989  mulcn2  12080  climaddc1  12097  climmulc2  12099  climsubc1  12100  climsubc2  12101  iserex  12107  climlec2  12109  iser3shft  12114  climcvg1nlem  12117  serf0  12120  sumrbdc  12148  fsumm1  12185  fsump1  12189  fsum00  12231  telfsumo  12235  fsumparts  12239  hashiun  12247  binomlem  12252  binom1dif  12256  bcxmas  12258  isumsplit  12260  isum1p  12261  arisum  12267  arisum2  12268  trireciplem  12269  explecnv  12274  geolim  12280  georeclim  12282  mertenslem2  12305  mertensabs  12306  prodf1f  12312  prodrbdclem2  12342  efcllemp  12427  ef0lem  12429  efgt0  12453  eftlub  12459  efsep  12460  effsumlt  12461  tanval3ap  12483  efi4p  12486  resin4p  12487  recos4p  12488  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  sinltxirr  12530  sin01gt0  12531  cos01gt0  12532  absefib  12540  efieq1re  12541  eirraplem  12546  dvdsdc  12567  dvdscmulr  12589  fsumdvds  12611  dvdslelemd  12612  3dvds  12633  odd2np1lem  12641  odd2np1  12642  flodddiv4  12705  bitsfzo  12724  bitsmod  12725  gcdsupex  12736  gcdsupcl  12737  gcd1  12766  nninfctlemfo  12819  nn0seqcvgd  12821  algcvg  12828  algcvgblem  12829  eucalg  12839  prmind2  12900  qden1elz  12985  dfphi2  13000  phiprm  13003  phimullem  13005  prmdiv  13015  prmdiveq  13016  prm23lt5  13044  pcpre1  13073  pczpre  13078  pcdiv  13083  pc1  13086  pcqdiv  13088  pcexp  13090  pcxnn0cl  13091  pcxcl  13092  pcdvdstr  13108  pc2dvds  13111  sumhashdc  13128  fldivp1  13129  pcfaclem  13130  qexpz  13133  expnprm  13134  prmpwdvds  13136  pockthlem  13137  4sqlem5  13163  4sqlem6  13164  4sqlem11  13182  4sqlem13m  13184  4sqlem19  13190  ballotfilemofi  13221  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemodife  13242  ballotfilemscl  13249  ballotfilemsle  13250  oddennn  13285  xpct  13289  ennnfonelemj0  13294  ennnfonelemen  13314  ctinfomlemom  13320  omctfn  13336  restid  13606  imasbas  13630  imasplusg  13631  imasmulr  13632  imasaddfnlemg  13637  xpscf  13670  gzsumvalx  13711  gzsumsplit1r  13717  gzsumcl  13806  mulgnngzsum  13932  mulgnndir  13956  mulgneg2  13961  gsumvalfi  14154  prdsex  14174  prdsval  14175  prdsbaslemss  14176  prdsbas  14178  prdsgrpd  14199  prdsinvgd  14200  dvdsrmuld  14405  zsssubrg  14924  znval  14973  znle  14974  znbaslemnn  14976  znf1o  14988  znleval  14990  psrval  15052  restuni2  15280  cnrest2r  15340  lmfss  15347  lmres  15351  lmtopcnp  15353  ispsmet  15426  isxmet2d  15451  ismet2  15457  blfvalps  15488  blex  15490  xblss2  15508  reopnap  15649  divcnap  15668  climcncf  15687  cncfmpt2fcntop  15702  hovera  15750  limcdifap  15765  cnplimcim  15770  cnlimcim  15774  cnlimc  15775  cnlimci  15776  dvbss  15788  dvcnp2cntop  15802  dvcn  15803  dvaddxxbr  15804  dvmulxxbr  15805  dvexp  15814  dveflem  15829  plyval  15835  elply2  15838  plyf  15840  plyss  15841  plyssc  15842  elplyr  15843  plyaddlem1  15850  plymullem1  15851  plyaddlem  15852  plymullem  15853  plyco  15862  plycj  15864  dvply1  15868  reeff1olem  15874  sinperlem  15912  sin2kpi  15915  cos2kpi  15916  sin2pim  15917  cos2pim  15918  cosq14gt0  15936  coseq0q4123  15938  tangtx  15942  abssinper  15950  sinkpi  15951  coskpi  15952  cosq34lt1  15954  logrpap0b  15981  logdivlti  15986  rpcxpsqrtth  16038  rpabscxpbnd  16048  binom4  16087  birthdaylem2  16094  birthdaylem3  16095  wilthlem1  16100  0sgm  16105  1sgmprm  16114  1sgm2ppw  16115  mersenne  16117  perfect1  16118  perfectlem1  16119  perfectlem2  16120  perfect  16121  bcp1ctr  16126  bclbnd  16127  lgslem1  16131  lgsval  16135  lgsfvalg  16136  lgsfcl2  16137  lgsfcl  16139  lgsval2lem  16141  lgsvalmod  16150  lgsneg  16155  lgsdilem  16158  lgsdir2lem3  16161  lgsdir  16166  lgsdilem2  16167  lgsdi  16168  lgsne0  16169  lgsabs1  16170  lgsprme0  16173  lgsdirnn0  16178  lgsdinn0  16179  gausslemma2dlem0d  16183  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  gausslemma2dlem3  16194  gausslemma2dlem4  16195  gausslemma2dlem5a  16196  gausslemma2dlem5  16197  gausslemma2dlem6  16198  lgseisenlem2  16202  lgseisen  16205  lgsquadlem1  16208  lgsquadlem2  16209  lgsquad2lem1  16212  lgsquad2lem2  16213  lgsquad2  16214  m1lgs  16216  2lgslem1  16222  2lgslem2  16223  2lgs  16235  2sqlem9  16255  2sqlem10  16256  ushgredgedg  16479  ushgredgedgloop  16481  uhgrspansubgrlem  16529  wlkvtxiedg  16598  wlkvtxiedgg  16599  wlk1walkdom  16612  upgr2wlkdc  16630  clwwlkccatlem  16653  umgrclwwlkge2  16655  clwwlknonmpo  16681  clwwlknonex2lem2  16691  clwwlknonex2  16692  konigsberglem1  16741  pwle2  17040  pw1nct  17045  nninfsellemdc  17065  nnnninfen  17076  nnnninfex  17077  nninfnfiinf  17078  sbthom  17083  repiecelem  17086  repiecele0  17087  trirec0  17105  apdifflemr  17108  reap0  17120  nconstwlpolem  17127