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  1805  sseqtrid  3274  ssdifin0  3573  uneqdifeqim  3577  unimax  3922  opth  4324  djussxp  4870  iss  5054  relresfld  5261  eldmrexrn  5781  f1oresrab  5805  fmptco  5806  fsn  5812  fnressn  5832  foima2  5884  foeqcnvco  5923  isoini2  5952  relmptopab  6216  ofres  6242  ofco  6246  tposexg  6415  tfrlemisucaccv  6482  tfrlemibex  6486  tfri1dALT  6508  tfrcl  6521  rdgivallem  6538  frecabex  6555  frectfr  6557  frecrdg  6565  pmresg  6836  mapsn  6850  mapsncnv  6855  ixpsnf1o  6896  en1  6964  2dom  6971  enpr2d  6985  en2  6986  mapxpen  7022  phplem4  7029  exmidpw2en  7090  fiintim  7109  sbthlem2  7141  elfir  7156  infglbti  7208  caseinl  7274  caseinr  7275  difinfsnlem  7282  difinfsn  7283  nninfisollemne  7314  exmidfodomrlemim  7395  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  2omotaplemap  7459  archnqq  7620  prarloclemlt  7696  prarloclemlo  7697  prarloclemcalc  7705  recexprlemm  7827  recexprlemex  7840  caucvgprlemm  7871  caucvgprprlemmu  7898  suplocexprlem2b  7917  suplocexprlemmu  7921  suplocexprlemlub  7927  1idsr  7971  recexgt0sr  7976  archsr  7985  caucvgsrlemoffval  7999  caucvgsrlemofff  8000  caucvgsrlemoffres  8003  caucvgsr  8005  ltpsrprg  8006  suplocsrlem  8011  pitonnlem2  8050  pitonn  8051  pitoregt0  8052  pitore  8053  recnnre  8054  axrnegex  8082  nntopi  8097  msqge0  8779  mulge0  8782  recexaplem2  8815  recexap  8816  recgt0  9013  recreclt  9063  nn1m1nn  9144  nn1suc  9145  nnle1eq1  9150  nn1gt1  9160  nnsub  9165  addltmul  9364  nn0le0eq0  9413  elnn0nn  9427  elnnz  9472  elznn0  9477  zlem1lt  9519  zltlem1  9520  elz2  9534  nn0n0n1ge2b  9542  nn0lt2  9544  nn0le2is012  9545  eluzaddi  9766  eluzsubi  9767  uzp1  9773  peano2uzr  9797  nn01to3  9829  qreccl  9854  irrmulap  9860  ltpnf  9993  xaddass2  10083  iccen  10219  fz01en  10266  fzpreddisj  10284  fzsuc2  10292  fseq1p1m1  10307  fseq1m1p1  10308  elfzp1b  10310  fzoss2  10387  fzval3  10427  fzosplitsnm1  10432  fzosplitprm1  10457  flhalf  10539  fldiv4lem1div2uz2  10543  modqmulnn  10581  modqmuladdnn0  10607  frec2uzrand  10644  frecuzrdg0  10652  frecuzrdg0t  10661  frecfzennn  10665  frecfzen2  10666  uzennn  10675  seqeq1  10689  seqp1g  10705  seqclg  10711  seq3m1  10712  monoord2  10725  ser3mono  10726  seqf1oglem1  10758  seqf1oglem2  10759  seqfeq4g  10770  ser0f  10773  exp3vallem  10779  expm1t  10806  expeq0  10809  expubnd  10835  binom3  10896  facndiv  10978  facavg  10985  bcn0  10994  bcnp1n  10998  bcm1k  10999  bcp1nk  11001  bcval5  11002  bcn2  11003  bcp1m1  11004  bcpasc  11005  bcn2m1  11008  hashsng  11037  hashun  11044  hashfz  11061  hashfzo  11062  seq3coll  11082  hash2en  11083  iswrdiz  11096  snopiswrd  11099  ccat1st1st  11193  swrds1  11221  cats1un  11274  wrdind  11275  wrd2ind  11276  swrdccatin1  11278  swrdccat3blem  11292  shftfval  11353  2shfti  11363  resqrexlemf1  11540  abs00ap  11594  sqabs  11614  ltabs  11619  caubnd2  11649  max0addsup  11751  rexico  11753  mulcn2  11844  climaddc1  11861  climmulc2  11863  climsubc1  11864  climsubc2  11865  iserex  11871  climlec2  11873  iser3shft  11878  climcvg1nlem  11881  serf0  11884  sumrbdc  11911  fsumm1  11948  fsump1  11952  fsum00  11994  telfsumo  11998  fsumparts  12002  hashiun  12010  binomlem  12015  binom1dif  12019  bcxmas  12021  isumsplit  12023  isum1p  12024  arisum  12030  arisum2  12031  trireciplem  12032  explecnv  12037  geolim  12043  georeclim  12045  mertenslem2  12068  mertensabs  12069  prodf1f  12075  prodrbdclem2  12105  efcllemp  12190  ef0lem  12192  efgt0  12216  eftlub  12222  efsep  12223  effsumlt  12224  tanval3ap  12246  efi4p  12249  resin4p  12250  recos4p  12251  ef01bndlem  12288  sin01bnd  12289  cos01bnd  12290  sinltxirr  12293  sin01gt0  12294  cos01gt0  12295  absefib  12303  efieq1re  12304  eirraplem  12309  dvdsdc  12330  dvdscmulr  12352  fsumdvds  12374  dvdslelemd  12375  3dvds  12396  odd2np1lem  12404  odd2np1  12405  flodddiv4  12468  bitsfzo  12487  bitsmod  12488  gcdsupex  12499  gcdsupcl  12500  gcd1  12529  nninfctlemfo  12582  nn0seqcvgd  12584  algcvg  12591  algcvgblem  12592  eucalg  12602  prmind2  12663  qden1elz  12748  dfphi2  12763  phiprm  12766  phimullem  12768  prmdiv  12778  prmdiveq  12779  prm23lt5  12807  pcpre1  12836  pczpre  12841  pcdiv  12846  pc1  12849  pcqdiv  12851  pcexp  12853  pcxnn0cl  12854  pcxcl  12855  pcdvdstr  12871  pc2dvds  12874  sumhashdc  12891  fldivp1  12892  pcfaclem  12893  qexpz  12896  expnprm  12897  prmpwdvds  12899  pockthlem  12900  4sqlem5  12926  4sqlem6  12927  4sqlem11  12945  4sqlem13m  12947  4sqlem19  12953  oddennn  12984  xpct  12988  ennnfonelemj0  12993  ennnfonelemen  13013  ctinfomlemom  13019  omctfn  13035  restid  13304  prdsex  13323  prdsval  13327  prdsbaslemss  13328  prdsbas  13330  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfnlemg  13368  xpscf  13401  igsumvalx  13443  gsumsplit1r  13452  gsumprval  13453  gsumfzz  13549  gsumfzcl  13553  prdsgrpd  13663  prdsinvgd  13664  mulgnngsum  13685  mulgnndir  13709  mulgneg2  13714  dvdsrmuld  14081  zsssubrg  14570  znval  14621  znle  14622  znbaslemnn  14624  znf1o  14636  znleval  14638  psrval  14651  restuni2  14872  cnrest2r  14932  lmfss  14939  lmres  14943  lmtopcnp  14945  ispsmet  15018  isxmet2d  15043  ismet2  15049  blfvalps  15080  blex  15082  xblss2  15100  reopnap  15241  divcnap  15260  climcncf  15279  cncfmpt2fcntop  15294  hovera  15342  limcdifap  15357  cnplimcim  15362  cnlimcim  15366  cnlimc  15367  cnlimci  15368  dvbss  15380  dvcnp2cntop  15394  dvcn  15395  dvaddxxbr  15396  dvmulxxbr  15397  dvexp  15406  dveflem  15421  plyval  15427  elply2  15430  plyf  15432  plyss  15433  plyssc  15434  elplyr  15435  plyaddlem1  15442  plymullem1  15443  plyaddlem  15444  plymullem  15445  plyco  15454  plycj  15456  dvply1  15460  reeff1olem  15466  sinperlem  15503  sin2kpi  15506  cos2kpi  15507  sin2pim  15508  cos2pim  15509  cosq14gt0  15527  coseq0q4123  15529  tangtx  15533  abssinper  15541  sinkpi  15542  coskpi  15543  cosq34lt1  15545  logrpap0b  15571  logdivlti  15576  rpcxpsqrtth  15625  rpabscxpbnd  15635  binom4  15674  wilthlem1  15675  0sgm  15680  1sgmprm  15689  1sgm2ppw  15690  mersenne  15692  perfect1  15693  perfectlem1  15694  perfectlem2  15695  perfect  15696  lgslem1  15700  lgsval  15704  lgsfvalg  15705  lgsfcl2  15706  lgsfcl  15708  lgsval2lem  15710  lgsvalmod  15719  lgsneg  15724  lgsdilem  15727  lgsdir2lem3  15730  lgsdir  15735  lgsdilem2  15736  lgsdi  15737  lgsne0  15738  lgsabs1  15739  lgsprme0  15742  lgsdirnn0  15747  lgsdinn0  15748  gausslemma2dlem0d  15752  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  gausslemma2dlem3  15763  gausslemma2dlem4  15764  gausslemma2dlem5a  15765  gausslemma2dlem5  15766  gausslemma2dlem6  15767  lgseisenlem2  15771  lgseisen  15774  lgsquadlem1  15777  lgsquadlem2  15778  lgsquad2lem1  15781  lgsquad2lem2  15782  lgsquad2  15783  m1lgs  15785  2lgslem1  15791  2lgslem2  15792  2lgs  15804  2sqlem9  15824  2sqlem10  15825  ushgredgedg  16045  ushgredgedgloop  16047  wlkvtxiedg  16117  wlkvtxiedgg  16118  wlk1walkdom  16131  upgr2wlkdc  16147  clwwlkccatlem  16169  umgrclwwlkge2  16171  2omap  16472  pwle2  16477  pw1nct  16482  nninfsellemdc  16490  nnnninfen  16501  nnnninfex  16502  nninfnfiinf  16503  sbthom  16508  trirec0  16526  apdifflemr  16529  reap0  16540  nconstwlpolem  16547