Theorem sylancr 406

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 404	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:  mpteq2da  3949  unipw  4068  opeluu  4300  uniexb  4323  unon  4356  onintrab2im  4363  xpexg  4581  resiexg  4790  imaexg  4819  exse2  4839  soirri  4859  djudisj  4892  elxp5  4953  cnvexg  5002  cnviinm  5006  coexg  5009  funssres  5090  f1oabexg  5300  sefvex  5361  ssimaex  5400  mptfvex  5424  f1ompt  5489  fmptcof  5504  resfunexg  5557  mptexg  5561  funfvima3  5567  ovid  5799  ov  5802  ofres  5907  cofunexg  5920  opabex3d  5930  opabex3  5931  oprabexd  5936  1stcof  5972  2ndcof  5973  mpt2exxg  6015  cnvf1o  6028  f2ndf  6029  algrflemg  6033  tposexg  6061  tfrlemisucaccv  6128  tfrlemibxssdm  6130  tfrlemibfn  6131  tfrlemi14d  6136  tfr1onlemsucaccv  6144  tfr1onlembxssdm  6146  tfr1onlembfn  6147  tfr1onlemres  6152  tfrcllemsucaccv  6157  tfrcllembxssdm  6159  tfrcllembfn  6160  tfrcllemres  6165  rdgtfr  6177  rdgruledefgg  6178  rdgon  6189  frecabex  6201  freccllem  6205  frecfcllem  6207  omcl  6262  oeicl  6263  erth  6376  th3qlem1  6434  mapex  6451  pmvalg  6456  mapsnconst  6491  ixpexgg  6519  fundmen  6603  cnvct  6606  snfig  6611  unen  6613  xpdom2  6627  mapxpen  6644  phplem2  6649  findcard2  6685  findcard2s  6686  infnfi  6691  relcnvfi  6730  sbthlemi8  6753  sbthlemi10  6755  djur  6837  casef  6859  caseinj  6860  caseinl  6862  djudom  6863  djuinj  6868  0ct  6869  ctmlemr  6870  enomnilem  6881  ltnnnq  7079  nnnq0lem1  7102  addnqprlemfl  7215  addnqprlemfu  7216  mulnqprlemfl  7231  mulnqprlemfu  7232  prsrlem1  7385  gt0srpr  7391  caucvgsrlemcl  7431  caucvgsrlemfv  7433  caucvgsrlembound  7436  mulcnsr  7469  mulcnsrec  7477  addvalex  7478  pitoregt0  7483  axmulass  7505  axdistr  7506  recriota  7522  mulid1  7582  axmulgt0  7655  cnegexlem2  7755  cnegex  7757  gt0ne0d  8087  recexre  8152  msqge0  8190  mulge0  8193  recgt0  8408  recreclt  8458  cju  8519  nnge1  8543  nnnlt1  8546  nn0nlt0  8797  elz2  8916  nnm1ge0  8931  recnz  8938  zneo  8946  uz3m2nn  9160  eluz2b2  9189  nn01to3  9201  mnflt  9352  xltadd1  9442  lincmb01cmp  9569  iccf1o  9570  fz1n  9607  fseq1p1m1  9657  fznn0  9676  fzctr  9693  4fvwrd4  9700  elfzonlteqm1  9770  divfl0  9852  modqelico  9890  zmodfz  9902  modqid  9905  modqmuladdim  9923  m1modge3gt1  9927  addmodid  9928  frec2uzf1od  9962  frecfzennn  9982  frecfzen2  9983  fzfig  9986  ser0  10064  ser3le  10068  expgt1  10108  expubnd  10127  iexpcyc  10174  binom2sub  10182  binom3  10186  zesq  10187  bernneq  10189  bernneq2  10190  expnbnd  10192  expnlbnd2  10194  facdiv  10261  faclbnd2  10265  faclbnd3  10266  bcval4  10275  hashinfom  10301  hashennn  10303  fihashf1rn  10312  isfinite4im  10316  hashfz  10344  crre  10406  crim  10407  remim  10409  mulreap  10413  cjreb  10415  recj  10416  reneg  10417  readd  10418  remullem  10420  imcj  10424  imneg  10425  imadd  10426  cjadd  10433  cjneg  10439  imval2  10443  cjreim  10452  cnrecnv  10459  uzin2  10535  absval  10549  rennim  10550  resqrexlemcalc3  10564  resqrexlemnm  10566  resqrexlemcvg  10567  resqrexlemgt0  10568  resqrexlemga  10571  absreimsq  10615  absreim  10616  amgm2  10666  climconst2  10834  climshft  10847  climshft2  10849  reccn2ap  10856  climge0  10868  sumsnf  10952  sumnul  10967  isumcl  10968  fsum2dlemstep  10977  fisumcom2  10981  fsumabs  11008  fsumiun  11020  binom  11027  bcxmas  11032  arisum  11041  expcnvap0  11045  explecnv  11048  geosergap  11049  geolim  11054  geolim2  11055  geo2sum  11057  geo2lim  11059  cvgratnnlemrate  11073  cvgratz  11075  mertenslemi1  11078  efcllemp  11097  ege2le3  11110  eftlub  11129  efgt1  11136  tanval2ap  11153  tanval3ap  11154  resinval  11155  recosval  11156  efi4p  11157  resin4p  11158  recos4p  11159  resincl  11160  recoscl  11161  efmival  11173  efeul  11174  sinadd  11176  cosadd  11177  tanaddap  11179  sinmul  11184  cos2tsin  11191  ef01bndlem  11196  sin01bnd  11197  cos01bnd  11198  sin01gt0  11201  cos01gt0  11202  absef  11208  absefib  11209  efieq1re  11210  demoivreALT  11212  eirraplem  11213  odd2np1  11300  oddm1even  11302  oddp1even  11303  oexpneg  11304  opoe  11322  omoe  11323  nn0o1gt2  11332  nn0o  11334  algcvg  11457  algcvgblem  11458  1nprm  11523  1idssfct  11524  oddprmge3  11543  divgcdodd  11549  pw2dvdslemn  11570  pw2dvds  11571  oddpwdclemodd  11577  oddpwdc  11579  phicl2  11617  phibndlem  11619  phibnd  11620  hashdvds  11624  crth  11627  phimullem  11628  hashgcdeq  11631  evenennn  11633  slotex  11670  setscom  11683  setsslid  11693  2strbas1g  11747  2strop1g  11748  rngbaseg  11759  rngplusgg  11760  rngmulrg  11761  srngbased  11766  srngplusgd  11767  srngmulrd  11768  srnginvld  11769  lmodbased  11777  lmodplusgd  11778  lmodscad  11779  lmodvscad  11780  ipsbased  11785  ipsaddgd  11786  ipsmulrd  11787  ipsscad  11788  ipsvscad  11789  ipsipd  11790  topgrpbasd  11795  topgrpplusgd  11796  topgrptsetd  11797  toponsspwpwg  11872  topgele  11879  istps  11882  topontopn  11887  tgvalex  11902  tgclb  11917  lmfval  12044  lmres  12099  ispsmet  12109  psmetge0  12117  ismet  12130  isxmet  12131  xmetge0  12151  isxms2  12238  comet  12285  bdxmet  12287  cnmetdval  12308  cnbl0  12311  cnblcld  12312  tgioo  12320