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  3846  unipw  3953  opeluu  4182  uniexb  4205  unon  4237  onintrab2im  4244  opeliunxp  4395  xpexg  4452  resiexg  4653  imaexg  4680  exse2  4699  soirri  4719  djudisj  4750  elxp5  4809  cnvexg  4855  cnviinm  4859  coexg  4862  funssres  4942  f1oabexg  5138  sefvex  5196  ssimaex  5234  mptfvex  5256  f1ompt  5320  fmptcof  5331  resfunexg  5382  mptexg  5386  funfvima3  5392  ovid  5617  ov  5620  ofres  5725  cofunexg  5738  opabex3d  5748  opabex3  5749  oprabexd  5754  1stcof  5790  2ndcof  5791  mpt2exxg  5833  cnvf1o  5846  f2ndf  5847  algrflemg  5851  tposexg  5873  tfrlemisucaccv  5939  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemi14d  5947  rdgtfr  5961  rdgruledefgg  5962  frecabex  5984  omcl  6041  erth  6150  th3qlem1  6208  fundmen  6286  snfig  6291  unen  6293  xpdom2  6305  phplem2  6316  findcard2  6346  findcard2s  6347  ltnnnq  6521  nnnq0lem1  6544  addnqprlemfl  6657  addnqprlemfu  6658  mulnqprlemfl  6673  mulnqprlemfu  6674  prsrlem1  6827  gt0srpr  6833  caucvgsrlemcl  6873  caucvgsrlemfv  6875  caucvgsrlembound  6878  mulcnsr  6911  mulcnsrec  6919  addvalex  6920  pitoregt0  6925  axmulass  6947  axdistr  6948  recriota  6964  mulid1  7024  axmulgt0  7091  cnegexlem2  7187  cnegex  7189  gt0ne0d  7504  recexre  7569  msqge0  7607  mulge0  7610  recgt0  7816  recreclt  7866  cju  7913  nnge1  7937  nnnlt1  7940  nn0nlt0  8208  elz2  8312  nnm1ge0  8326  recnz  8333  zneo  8339  uz3m2nn  8515  eluz2b2  8540  nn01to3  8552  mnflt  8704  lincmb01cmp  8871  iccf1o  8872  fz1n  8908  fseq1p1m1  8956  fznn0  8974  fzctr  8991  4fvwrd4  8997  elfzonlteqm1  9066  divfl0  9138  modqelico  9176  frec2uzf1od  9192  frecuzrdgrom  9196  frecfzennn  9203  frecfzen2  9204  fzfig  9206  iser0  9250  serile  9253  expgt1  9293  expubnd  9311  binom2sub  9364  binom3  9366  zesq  9367  bernneq  9369  bernneq2  9370  expnbnd  9372  expnlbnd2  9374  crre  9457  crim  9458  remim  9460  mulreap  9464  cjreb  9466  recj  9467  reneg  9468  readd  9469  remullem  9471  imcj  9475  imneg  9476  imadd  9477  cjadd  9484  cjneg  9490  imval2  9494  cjreim  9503  cnrecnv  9510  uzin2  9586  absval  9599  rennim  9600  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemgt0  9618  resqrexlemga  9621  absreimsq  9665  absreim  9666  amgm2  9714  climconst2  9812  climshft  9825  climshft2  9827  climge0  9845  ialgcvg  9887  algcvgblem  9888