Theorem sylancl 407

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  sylanblc  409  sylanblrc  410  equveli  1700  syl5sseq  3097  ssdifin0  3391  uneqdifeqim  3395  unimax  3717  opth  4097  djussxp  4622  iss  4801  relresfld  5004  eldmrexrn  5493  f1oresrab  5517  fmptco  5518  fsn  5524  fnressn  5538  foima2  5585  foeqcnvco  5623  isoini2  5652  ofres  5927  ofco  5931  tposexg  6085  tfrlemisucaccv  6152  tfrlemibex  6156  tfri1dALT  6178  tfrcl  6191  rdgivallem  6208  frecabex  6225  frectfr  6227  frecrdg  6235  pmresg  6500  mapsn  6514  mapsncnv  6519  ixpsnf1o  6560  en1  6623  2dom  6629  mapxpen  6671  phplem4  6678  fiintim  6746  sbthlem2  6774  infglbti  6827  caseinl  6891  caseinr  6892  difinfsnlem  6899  difinfsn  6900  exmidfodomrlemim  6966  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  archnqq  7126  prarloclemlt  7202  prarloclemlo  7203  prarloclemcalc  7211  recexprlemm  7333  recexprlemex  7346  caucvgprlemm  7377  caucvgprprlemmu  7404  1idsr  7464  recexgt0sr  7469  archsr  7477  caucvgsrlemoffval  7491  caucvgsrlemofff  7492  caucvgsrlemoffres  7495  caucvgsr  7497  pitonnlem2  7534  pitonn  7535  pitoregt0  7536  pitore  7537  recnnre  7538  axrnegex  7564  nntopi  7579  msqge0  8244  mulge0  8247  recexaplem2  8274  recexap  8275  recgt0  8466  recreclt  8516  nn1m1nn  8596  nn1suc  8597  nnle1eq1  8602  nn1gt1  8612  nnsub  8617  addltmul  8808  nn0le0eq0  8857  elnn0nn  8871  elnnz  8916  elznn0  8921  zlem1lt  8962  zltlem1  8963  elz2  8974  nn0n0n1ge2b  8982  nn0lt2  8984  nn0le2is012  8985  eluzaddi  9202  eluzsubi  9203  uzp1  9209  peano2uzr  9230  nn01to3  9259  qreccl  9284  ltpnf  9408  xaddass2  9494  fz01en  9674  fzpreddisj  9692  fzsuc2  9700  fseq1p1m1  9715  fseq1m1p1  9716  elfzp1b  9718  fzoss2  9790  fzval3  9822  fzosplitsnm1  9827  fzosplitprm1  9852  flhalf  9916  modqmulnn  9956  modqmuladdnn0  9982  frec2uzrand  10019  frecuzrdg0  10027  frecuzrdg0t  10036  frecfzennn  10040  frecfzen2  10041  uzennn  10050  seqeq1  10062  seq3m1  10082  monoord2  10091  ser3mono  10092  ser0f  10129  exp3vallem  10135  expm1t  10162  expeq0  10165  expubnd  10191  binom3  10250  facndiv  10326  facavg  10333  bcn0  10342  bcnp1n  10346  bcm1k  10347  bcp1nk  10349  bcval5  10350  bcn2  10351  bcp1m1  10352  bcpasc  10353  bcn2m1  10356  hashsng  10385  hashun  10392  hashfz  10408  hashfzo  10409  seq3coll  10426  shftfval  10434  2shfti  10444  resqrexlemf1  10620  abs00ap  10674  sqabs  10694  ltabs  10699  caubnd2  10729  max0addsup  10831  rexico  10833  mulcn2  10920  climaddc1  10937  climmulc2  10939  climsubc1  10940  climsubc2  10941  iserex  10947  climlec2  10949  iser3shft  10954  climcvg1nlem  10957  serf0  10960  sumrbdc  10986  fsumm1  11024  fsump1  11028  fsum00  11070  telfsumo  11074  fsumparts  11078  hashiun  11086  binomlem  11091  binom1dif  11095  bcxmas  11097  isumsplit  11099  isum1p  11100  arisum  11106  arisum2  11107  trireciplem  11108  explecnv  11113  geolim  11119  georeclim  11121  mertenslem2  11144  mertensabs  11145  efcllemp  11162  ef0lem  11164  efgt0  11188  eftlub  11194  efsep  11195  effsumlt  11196  tanval3ap  11219  efi4p  11222  resin4p  11223  recos4p  11224  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  sin01gt0  11266  cos01gt0  11267  absefib  11274  efieq1re  11275  eirraplem  11278  dvdsdc  11296  dvdscmulr  11317  dvdslelemd  11336  odd2np1lem  11364  odd2np1  11365  flodddiv4  11426  gcdsupex  11441  gcdsupcl  11442  gcd1  11470  nn0seqcvgd  11515  algcvg  11522  algcvgblem  11523  eucalg  11533  prmind2  11594  qden1elz  11675  dfphi2  11688  phiprm  11691  phimullem  11693  oddennn  11697  xpct  11701  ennnfonelemj0  11706  ennnfonelemen  11726  ctinfomlemom  11732  restid  11913  restuni2  12128  cnrest2r  12187  lmfss  12194  lmres  12198  lmtopcnp  12200  ispsmet  12251  isxmet2d  12276  ismet2  12282  blfvalps  12313  blex  12315  xblss2  12333  climcncf  12484  limcdifap  12512  cnplimcim  12516  cnlimcim  12517  cnlimci  12518  dvbss  12527  pwle2  12779  nninfsellemdc  12790  sbthom  12805