Theorem sylancr 405

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mpteq2da  3867  unipw  3972  opeluu  4200  uniexb  4223  unon  4255  onintrab2im  4262  xpexg  4470  resiexg  4673  imaexg  4700  exse2  4719  soirri  4739  djudisj  4770  elxp5  4829  cnvexg  4875  cnviinm  4879  coexg  4882  funssres  4962  f1oabexg  5158  sefvex  5216  ssimaex  5255  mptfvex  5277  f1ompt  5341  fmptcof  5352  resfunexg  5403  mptexg  5407  funfvima3  5413  ovid  5637  ov  5640  ofres  5745  cofunexg  5758  opabex3d  5768  opabex3  5769  oprabexd  5774  1stcof  5810  2ndcof  5811  mpt2exxg  5853  cnvf1o  5866  f2ndf  5867  algrflemg  5871  tposexg  5896  tfrlemisucaccv  5962  tfrlemibxssdm  5964  tfrlemibfn  5965  tfrlemi14d  5970  rdgtfr  5984  rdgruledefgg  5985  frecabex  6007  omcl  6064  erth  6173  th3qlem1  6231  fundmen  6309  snfig  6314  unen  6316  xpdom2  6328  phplem2  6339  findcard2  6373  findcard2s  6374  relcnvfi  6391  ltnnnq  6613  nnnq0lem1  6636  addnqprlemfl  6749  addnqprlemfu  6750  mulnqprlemfl  6765  mulnqprlemfu  6766  prsrlem1  6919  gt0srpr  6925  caucvgsrlemcl  6965  caucvgsrlemfv  6967  caucvgsrlembound  6970  mulcnsr  7003  mulcnsrec  7011  addvalex  7012  pitoregt0  7017  axmulass  7039  axdistr  7040  recriota  7056  mulid1  7116  axmulgt0  7184  cnegexlem2  7284  cnegex  7286  gt0ne0d  7613  recexre  7678  msqge0  7716  mulge0  7719  recgt0  7928  recreclt  7978  cju  8038  nnge1  8062  nnnlt1  8065  nn0nlt0  8314  elz2  8419  nnm1ge0  8433  recnz  8440  zneo  8448  uz3m2nn  8661  eluz2b2  8690  nn01to3  8702  mnflt  8858  lincmb01cmp  9025  iccf1o  9026  fz1n  9063  fseq1p1m1  9111  fznn0  9129  fzctr  9144  4fvwrd4  9150  elfzonlteqm1  9219  divfl0  9298  modqelico  9336  zmodfz  9348  modqid  9351  modqmuladdim  9369  m1modge3gt1  9373  addmodid  9374  frec2uzf1od  9408  frecuzrdgrom  9412  frecfzennn  9419  frecfzen2  9420  fzfig  9422  iser0  9471  serile  9474  expgt1  9514  expubnd  9533  iexpcyc  9579  binom2sub  9587  binom3  9590  zesq  9591  bernneq  9593  bernneq2  9594  expnbnd  9596  expnlbnd2  9598  facdiv  9665  faclbnd2  9669  faclbnd3  9670  bcval4  9679  crre  9744  crim  9745  remim  9747  mulreap  9751  cjreb  9753  recj  9754  reneg  9755  readd  9756  remullem  9758  imcj  9762  imneg  9763  imadd  9764  cjadd  9771  cjneg  9777  imval2  9781  cjreim  9790  cnrecnv  9797  uzin2  9873  absval  9887  rennim  9888  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemgt0  9906  resqrexlemga  9909  absreimsq  9953  absreim  9954  amgm2  10004  climconst2  10130  climshft  10143  climshft2  10145  climge0  10163  odd2np1  10272  oddm1even  10274  oddp1even  10275  oexpneg  10276  opoe  10295  omoe  10296  nn0o1gt2  10305  nn0o  10307  ialgcvg  10430  algcvgblem  10431  1nprm  10496  1idssfct  10497  oddprmge3  10516  divgcdodd  10522  pw2dvdslemn  10543  pw2dvds  10544  oddpwdclemodd  10550  oddpwdc  10552