Theorem sylancr 412

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpteq2da  4076  unipw  4200  opeluu  4433  uniexb  4456  unon  4493  onintrab2im  4500  xpexg  4723  resiexg  4934  imaexg  4963  exse2  4983  soirri  5003  djudisj  5036  elxp5  5097  cnvexg  5146  cnviinm  5150  coexg  5153  funssres  5238  f1oabexg  5452  sefvex  5515  ssimaex  5555  mptfvex  5579  f1ompt  5644  fmptcof  5660  resfunexg  5714  mptexg  5718  funfvima3  5726  ovid  5966  ov  5969  ofres  6072  cofunexg  6085  opabex3d  6097  opabex3  6098  oprabexd  6103  1stcof  6139  2ndcof  6140  mpoexxg  6186  cnvf1o  6201  f2ndf  6202  algrflemg  6206  tposexg  6234  tfrlemisucaccv  6301  tfrlemibxssdm  6303  tfrlemibfn  6304  tfrlemi14d  6309  tfr1onlemsucaccv  6317  tfr1onlembxssdm  6319  tfr1onlembfn  6320  tfr1onlemres  6325  tfrcllemsucaccv  6330  tfrcllembxssdm  6332  tfrcllembfn  6333  tfrcllemres  6338  rdgtfr  6350  rdgruledefgg  6351  rdgon  6362  frecabex  6374  freccllem  6378  frecfcllem  6380  omcl  6437  oeicl  6438  erth  6553  th3qlem1  6611  mapex  6628  pmvalg  6633  mapsnconst  6668  ixpexgg  6696  fundmen  6780  cnvct  6783  snfig  6788  unen  6790  xpdom2  6805  mapxpen  6822  phplem2  6827  findcard2  6863  findcard2s  6864  infnfi  6869  relcnvfi  6914  sbthlemi8  6937  sbthlemi10  6939  fival  6943  fiss  6950  inl11  7038  casef  7061  caseinj  7062  caseinl  7064  caseinr  7065  djudom  7066  difinfsn  7073  djuinj  7079  0ct  7080  ctmlemr  7081  ctssdccl  7084  enomnilem  7110  enmkvlem  7133  enwomnilem  7141  djuassen  7181  xpdjuen  7182  djudoml  7183  djudomr  7184  cc2lem  7215  ltnnnq  7372  nnnq0lem1  7395  addnqprlemfl  7508  addnqprlemfu  7509  mulnqprlemfl  7524  mulnqprlemfu  7525  suplocexprlem2b  7663  prsrlem1  7691  gt0srpr  7697  caucvgsrlemcl  7738  caucvgsrlemfv  7740  caucvgsrlembound  7743  mulcnsr  7784  mulcnsrec  7792  addvalex  7793  pitoregt0  7798  axmulass  7822  axdistr  7823  recriota  7839  mulid1  7904  axmulgt0  7978  cnegexlem2  8082  cnegex  8084  gt0ne0d  8418  recexre  8484  msqge0  8522  mulge0  8525  recgt0  8753  recreclt  8803  cju  8864  nnge1  8888  nnnlt1  8891  nn0nlt0  9148  elz2  9270  nnm1ge0  9285  recnz  9292  zneo  9300  uz3m2nn  9519  eluz2b2  9549  nn01to3  9563  mnflt  9727  xnn0dcle  9746  xltadd1  9820  lincmb01cmp  9947  iccf1o  9948  fz1n  9987  fseq1p1m1  10037  fznn0  10056  fzctr  10076  4fvwrd4  10083  elfzonlteqm1  10153  divfl0  10239  modqelico  10277  zmodfz  10289  modqid  10292  modqmuladdim  10310  m1modge3gt1  10314  addmodid  10315  frec2uzf1od  10349  frecfzennn  10369  frecfzen2  10370  fzfig  10373  ser0  10457  ser3le  10461  expgt1  10501  expubnd  10520  iexpcyc  10567  binom2sub  10576  binom3  10580  zesq  10581  bernneq  10583  bernneq2  10584  expnbnd  10586  expnlbnd2  10588  facdiv  10659  faclbnd2  10663  faclbnd3  10664  bcval4  10673  hashinfom  10699  hashennn  10701  fihashf1rn  10710  isfinite4im  10714  hashfz  10743  crre  10808  crim  10809  remim  10811  mulreap  10815  cjreb  10817  recj  10818  reneg  10819  readd  10820  remullem  10822  imcj  10826  imneg  10827  imadd  10828  cjadd  10835  cjneg  10841  imval2  10845  cjreim  10854  cnrecnv  10861  uzin2  10938  absval  10952  rennim  10953  resqrexlemcalc3  10967  resqrexlemnm  10969  resqrexlemcvg  10970  resqrexlemgt0  10971  resqrexlemga  10974  absreimsq  11018  absreim  11019  amgm2  11069  climconst2  11241  climshft  11254  climshft2  11256  reccn2ap  11263  climge0  11275  sumsnf  11359  sumnul  11374  isumcl  11375  fsum2dlemstep  11384  fisumcom2  11388  fsumabs  11415  fsumiun  11427  binom  11434  bcxmas  11439  arisum  11448  expcnvap0  11452  explecnv  11455  geosergap  11456  geolim  11461  geolim2  11462  geo2sum  11464  geo2lim  11466  cvgratnnlemrate  11480  cvgratz  11482  mertenslemi1  11485  prodf1  11492  prodeq2w  11506  fprodntrivap  11534  prodsnf  11542  fprod2dlemstep  11572  fprodcom2fi  11576  efcllemp  11608  ege2le3  11621  eftlub  11640  efgt1  11647  tanval2ap  11663  tanval3ap  11664  resinval  11665  recosval  11666  efi4p  11667  resin4p  11668  recos4p  11669  resincl  11670  recoscl  11671  efmival  11683  efeul  11684  sinadd  11686  cosadd  11687  tanaddap  11689  sinmul  11694  cos2tsin  11701  ef01bndlem  11706  sin01bnd  11707  cos01bnd  11708  sin01gt0  11711  cos01gt0  11712  absef  11719  absefib  11720  efieq1re  11721  demoivreALT  11723  eirraplem  11726  odd2np1  11819  oddm1even  11821  oddp1even  11822  oexpneg  11823  opoe  11841  omoe  11842  nn0o1gt2  11851  nn0o  11853  algcvg  11989  algcvgblem  11990  1nprm  12055  1idssfct  12056  oddprmge3  12076  divgcdodd  12084  pw2dvdslemn  12106  pw2dvds  12107  oddpwdclemodd  12113  oddpwdc  12115  phicl2  12155  phibndlem  12157  phibnd  12158  hashdvds  12162  crth  12165  phimullem  12166  eulerthlemfi  12169  eulerthlemrprm  12170  eulerthlema  12171  hashgcdeq  12180  phisum  12181  oddprm  12200  prm23ge5  12205  pythagtriplem1  12206  pythagtriplem4  12209  pythagtriplem12  12216  pythagtriplem14  12218  pczpre  12238  pcadd  12280  pcmpt  12282  pockthlem  12295  pockthi  12297  infpnlem2  12299  gzreim  12318  evenennn  12335  ennnfonelemj0  12343  ennnfonelemjn  12344  ennnfonelemg  12345  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemnn0  12364  exmidunben  12368  ctinfomlemom  12369  ssnnctlemct  12388  nninfdc  12395  slotex  12430  setscom  12443  setsslid  12453  basmex  12461  2strbas1g  12508  2strop1g  12509  rngbaseg  12520  rngplusgg  12521  rngmulrg  12522  srngbased  12527  srngplusgd  12528  srngmulrd  12529  srnginvld  12530  lmodbased  12538  lmodplusgd  12539  lmodscad  12540  lmodvscad  12541  ipsbased  12546  ipsaddgd  12547  ipsmulrd  12548  ipsscad  12549  ipsvscad  12550  ipsipd  12551  topgrpbasd  12556  topgrpplusgd  12557  topgrptsetd  12558  plusffvalg  12602  grpidvalg  12613  ismhm  12671  issubm  12681  0mhm  12690  toponsspwpwg  12735  topgele  12742  istps  12745  topontopn  12750  tgvalex  12765  tgclb  12780  lmfval  12907  lmres  12963  ispsmet  13038  psmetge0  13046  ismet  13059  isxmet  13060  xmetge0  13080  isxms2  13167  comet  13214  bdxmet  13216  cnmetdval  13244  cnbl0  13249  cnblcld  13250  reopnap  13253  tgioo  13261  cncfcncntop  13295  cncfmpt2fcntop  13300  limcimolemlt  13348  cnplimcim  13351  cnplimclemr  13353  limccnpcntop  13359  limccnp2lem  13360  limccnp2cntop  13361  dvfvalap  13365  dvbss  13369  dvcnp2cntop  13378  dvcn  13379  dvaddxxbr  13380  dvmulxxbr  13381  dvcoapbr  13386  dvcjbr  13387  dvrecap  13392  dveflem  13402  reeff1olem  13407  pilem3  13419  ef2kpi  13442  efper  13443  sinperlem  13444  efimpi  13455  ptolemy  13460  sincosq2sgn  13463  sincosq3sgn  13464  sincosq4sgn  13465  sinq12gt0  13466  cosq14gt0  13468  tangtx  13474  sinkpi  13483  coskpi  13484  cosordlem  13485  rplogcl  13515  logge0  13516  logdivlti  13517  logbleb  13594  logblt  13595  binom4  13612  lgsval2lem  13626  lgsval4a  13638  lgsneg  13640  lgsdilem  13643  lgsdirprm  13650  lgsdirnn0  13663  2sqlem2  13666  pwf1oexmid  13954  isomninnlem  13984  iswomninnlem  14003  ismkvnnlem  14006