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  1757  sseqtrid  3203  ssdifin0  3502  uneqdifeqim  3506  unimax  3839  opth  4231  djussxp  4765  iss  4946  relresfld  5150  eldmrexrn  5649  f1oresrab  5673  fmptco  5674  fsn  5680  fnressn  5694  foima2  5743  foeqcnvco  5781  isoini2  5810  ofres  6087  ofco  6091  tposexg  6249  tfrlemisucaccv  6316  tfrlemibex  6320  tfri1dALT  6342  tfrcl  6355  rdgivallem  6372  frecabex  6389  frectfr  6391  frecrdg  6399  pmresg  6666  mapsn  6680  mapsncnv  6685  ixpsnf1o  6726  en1  6789  2dom  6795  enpr2d  6807  mapxpen  6838  phplem4  6845  fiintim  6918  sbthlem2  6947  elfir  6962  infglbti  7014  caseinl  7080  caseinr  7081  difinfsnlem  7088  difinfsn  7089  nninfisollemne  7119  exmidfodomrlemim  7190  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  archnqq  7391  prarloclemlt  7467  prarloclemlo  7468  prarloclemcalc  7476  recexprlemm  7598  recexprlemex  7611  caucvgprlemm  7642  caucvgprprlemmu  7669  suplocexprlem2b  7688  suplocexprlemmu  7692  suplocexprlemlub  7698  1idsr  7742  recexgt0sr  7747  archsr  7756  caucvgsrlemoffval  7770  caucvgsrlemofff  7771  caucvgsrlemoffres  7774  caucvgsr  7776  ltpsrprg  7777  suplocsrlem  7782  pitonnlem2  7821  pitonn  7822  pitoregt0  7823  pitore  7824  recnnre  7825  axrnegex  7853  nntopi  7868  msqge0  8547  mulge0  8550  recexaplem2  8582  recexap  8583  recgt0  8778  recreclt  8828  nn1m1nn  8908  nn1suc  8909  nnle1eq1  8914  nn1gt1  8924  nnsub  8929  addltmul  9126  nn0le0eq0  9175  elnn0nn  9189  elnnz  9234  elznn0  9239  zlem1lt  9280  zltlem1  9281  elz2  9295  nn0n0n1ge2b  9303  nn0lt2  9305  nn0le2is012  9306  eluzaddi  9525  eluzsubi  9526  uzp1  9532  peano2uzr  9556  nn01to3  9588  qreccl  9613  ltpnf  9749  xaddass2  9839  iccen  9975  fz01en  10021  fzpreddisj  10039  fzsuc2  10047  fseq1p1m1  10062  fseq1m1p1  10063  elfzp1b  10065  fzoss2  10140  fzval3  10172  fzosplitsnm1  10177  fzosplitprm1  10202  flhalf  10270  modqmulnn  10310  modqmuladdnn0  10336  frec2uzrand  10373  frecuzrdg0  10381  frecuzrdg0t  10390  frecfzennn  10394  frecfzen2  10395  uzennn  10404  seqeq1  10416  seq3m1  10436  monoord2  10445  ser3mono  10446  ser0f  10483  exp3vallem  10489  expm1t  10516  expeq0  10519  expubnd  10545  binom3  10605  facndiv  10685  facavg  10692  bcn0  10701  bcnp1n  10705  bcm1k  10706  bcp1nk  10708  bcval5  10709  bcn2  10710  bcp1m1  10711  bcpasc  10712  bcn2m1  10715  hashsng  10744  hashun  10751  hashfz  10767  hashfzo  10768  seq3coll  10788  shftfval  10796  2shfti  10806  resqrexlemf1  10983  abs00ap  11037  sqabs  11057  ltabs  11062  caubnd2  11092  max0addsup  11194  rexico  11196  mulcn2  11286  climaddc1  11303  climmulc2  11305  climsubc1  11306  climsubc2  11307  iserex  11313  climlec2  11315  iser3shft  11320  climcvg1nlem  11323  serf0  11326  sumrbdc  11353  fsumm1  11390  fsump1  11394  fsum00  11436  telfsumo  11440  fsumparts  11444  hashiun  11452  binomlem  11457  binom1dif  11461  bcxmas  11463  isumsplit  11465  isum1p  11466  arisum  11472  arisum2  11473  trireciplem  11474  explecnv  11479  geolim  11485  georeclim  11487  mertenslem2  11510  mertensabs  11511  prodf1f  11517  prodrbdclem2  11547  efcllemp  11632  ef0lem  11634  efgt0  11658  eftlub  11664  efsep  11665  effsumlt  11666  tanval3ap  11688  efi4p  11691  resin4p  11692  recos4p  11693  ef01bndlem  11730  sin01bnd  11731  cos01bnd  11732  sin01gt0  11735  cos01gt0  11736  absefib  11744  efieq1re  11745  eirraplem  11750  dvdsdc  11771  dvdscmulr  11793  dvdslelemd  11814  odd2np1lem  11842  odd2np1  11843  flodddiv4  11904  gcdsupex  11923  gcdsupcl  11924  gcd1  11953  nn0seqcvgd  12006  algcvg  12013  algcvgblem  12014  eucalg  12024  prmind2  12085  qden1elz  12170  dfphi2  12185  phiprm  12188  phimullem  12190  prmdiv  12200  prmdiveq  12201  prm23lt5  12228  pcpre1  12257  pczpre  12262  pcdiv  12267  pc1  12270  pcqdiv  12272  pcexp  12274  pcxnn0cl  12275  pcxcl  12276  pcdvdstr  12291  pc2dvds  12294  sumhashdc  12310  fldivp1  12311  pcfaclem  12312  qexpz  12315  expnprm  12316  prmpwdvds  12318  pockthlem  12319  4sqlem5  12345  4sqlem6  12346  oddennn  12358  xpct  12362  ennnfonelemj0  12367  ennnfonelemen  12387  ctinfomlemom  12393  omctfn  12409  restid  12619  mulgnndir  12870  mulgneg2  12875  restuni2  13228  cnrest2r  13288  lmfss  13295  lmres  13299  lmtopcnp  13301  ispsmet  13374  isxmet2d  13399  ismet2  13405  blfvalps  13436  blex  13438  xblss2  13456  reopnap  13589  divcnap  13606  climcncf  13622  cncfmpt2fcntop  13636  limcdifap  13682  cnplimcim  13687  cnlimcim  13691  cnlimc  13692  cnlimci  13693  dvbss  13705  dvcnp2cntop  13714  dvcn  13715  dvaddxxbr  13716  dvmulxxbr  13717  dvexp  13726  dveflem  13738  reeff1olem  13743  sinperlem  13780  sin2kpi  13783  cos2kpi  13784  sin2pim  13785  cos2pim  13786  cosq14gt0  13804  coseq0q4123  13806  tangtx  13810  abssinper  13818  sinkpi  13819  coskpi  13820  cosq34lt1  13822  logrpap0b  13848  logdivlti  13853  rpcxpsqrtth  13901  rpabscxpbnd  13910  binom4  13948  lgslem1  13952  lgsval  13956  lgsfvalg  13957  lgsfcl2  13958  lgsfcl  13960  lgsval2lem  13962  lgsvalmod  13971  lgsneg  13976  lgsdilem  13979  lgsdir2lem3  13982  lgsdir  13987  lgsdilem2  13988  lgsdi  13989  lgsne0  13990  lgsabs1  13991  lgsprme0  13994  lgsdirnn0  13999  lgsdinn0  14000  2sqlem9  14011  2sqlem10  14012  pwle2  14288  pw1nct  14293  nninfsellemdc  14300  sbthom  14315  trirec0  14333  apdifflemr  14336  reap0  14347  nconstwlpolem  14353