Theorem sylancr 393

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancr.1	⊢ 𝜓
sylancr.2	⊢ (𝜑 → 𝜒)
sylancr.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylancr	⊢ (𝜑 → 𝜃)

Proof of Theorem sylancr

Step	Hyp	Ref	Expression
1		sylancr.1	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		sylancr.2	. 2 ⊢ (𝜑 → 𝜒)
4		sylancr.3	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	2, 3, 4	syl2anc 391	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 97

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

This theorem is referenced by:  mpteq2da  3843  unipw  3950  opeluu  4178  uniexb  4201  unon  4233  onintrab2im  4240  opeliunxp  4382  xpexg  4439  resiexg  4640  imaexg  4667  exse2  4686  soirri  4706  djudisj  4737  elxp5  4796  cnvexg  4842  cnviinm  4846  coexg  4849  funssres  4929  f1oabexg  5125  sefvex  5183  ssimaex  5221  mptfvex  5243  f1ompt  5307  fmptcof  5318  resfunexg  5369  mptexg  5373  funfvima3  5379  ovid  5604  ov  5607  ofres  5712  cofunexg  5725  opabex3d  5735  opabex3  5736  oprabexd  5741  1stcof  5777  2ndcof  5778  mpt2exxg  5820  cnvf1o  5833  f2ndf  5834  algrflemg  5838  tposexg  5860  tfrlemisucaccv  5926  tfrlemibxssdm  5928  tfrlemibfn  5929  tfrlemi14d  5934  rdgtfr  5948  rdgruledefgg  5949  frecabex  5971  omcl  6028  erth  6137  th3qlem1  6195  fundmen  6273  snfig  6278  unen  6280  xpdom2  6292  phplem2  6303  findcard2  6332  findcard2s  6333  ltnnnq  6502  nnnq0lem1  6525  addnqprlemfl  6638  addnqprlemfu  6639  mulnqprlemfl  6654  mulnqprlemfu  6655  prsrlem1  6808  gt0srpr  6814  caucvgsrlemcl  6854  caucvgsrlemfv  6856  caucvgsrlembound  6859  mulcnsr  6892  mulcnsrec  6900  addvalex  6901  pitoregt0  6906  axmulass  6928  axdistr  6929  recriota  6945  mulid1  7005  axmulgt0  7071  cnegexlem2  7167  cnegex  7169  gt0ne0d  7482  recexre  7545  msqge0  7583  mulge0  7586  recgt0  7792  recreclt  7842  cju  7889  nnge1  7913  nnnlt1  7916  nn0nlt0  8180  elz2  8284  nnm1ge0  8298  recnz  8305  zneo  8311  uz3m2nn  8487  eluz2b2  8512  nn01to3  8524  mnflt  8671  lincmb01cmp  8838  iccf1o  8839  fz1n  8875  fseq1p1m1  8923  fznn0  8941  fzctr  8958  4fvwrd4  8964  elfzonlteqm1  9033  frec2uzf1od  9070  frecuzrdgrom  9074  frecfzennn  9081  frecfzen2  9082  fzfig  9084  iser0  9128  serile  9131  expgt1  9171  expubnd  9189  binom2sub  9242  binom3  9244  zesq  9245  bernneq  9247  bernneq2  9248  expnbnd  9250  expnlbnd2  9252  crre  9335  crim  9336  remim  9338  mulreap  9342  cjreb  9344  recj  9345  reneg  9346  readd  9347  remullem  9349  imcj  9353  imneg  9354  imadd  9355  cjadd  9362  cjneg  9368  imval2  9372  cjreim  9381  cnrecnv  9388  uzin2  9464  absval  9477  rennim  9478  resqrexlemcalc3  9492  resqrexlemnm  9494  resqrexlemcvg  9495  resqrexlemgt0  9496  resqrexlemga  9499  absreimsq  9543  absreim  9544  amgm2  9592  climconst2  9689  climshft  9702  climshft2  9704  climge0  9722  ialgcvg  9764  algcvgblem  9765