ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl12anc Unicode version

Theorem syl12anc 1236
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
syl12anc.4  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
Assertion
Ref Expression
syl12anc  |-  ( ph  ->  ta )

Proof of Theorem syl12anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca32 310 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 14 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  syl22anc  1239  cocan1  5782  fliftfun  5791  isopolem  5817  f1oiso2  5822  caovcld  6022  caovcomd  6025  tfrlemisucaccv  6320  tfr1onlemsucaccv  6336  tfr1onlembxssdm  6338  tfrcllemsucaccv  6349  tfrcllembxssdm  6351  fidceq  6863  findcard2d  6885  diffifi  6888  tridc  6893  en2eqpr  6901  sbthlemi9  6958  supisolem  7001  ordiso2  7028  difinfsnlem  7092  difinfsn  7093  prarloclemup  7482  prarloc  7490  nqprl  7538  nqpru  7539  ltaddpr  7584  aptiprlemu  7627  archpr  7630  cauappcvgprlem2  7647  caucvgprlem2  7667  caucvgprprlem2  7697  suplocexprlemlub  7711  suplocexpr  7712  recexgt0sr  7760  archsr  7769  axpre-suploclemres  7888  conjmulap  8672  lerec2  8832  ledivp1  8846  cju  8904  nn2ge  8938  gtndiv  9334  supinfneg  9581  infsupneg  9582  z2ge  9810  iccssioo2  9930  fzrev3  10070  elfz1b  10073  exbtwnzlemstep  10231  exbtwnzlemex  10233  rebtwn2zlemstep  10236  rebtwn2z  10238  qbtwnre  10240  flqdiv  10304  frec2uzled  10412  seq3caopr  10466  iseqf1olemab  10472  iseqf1olemnanb  10473  expnegzap  10537  nn0ltexp2  10671  hashen  10745  hashunlem  10765  hashprg  10769  leisorel  10798  zfz1isolemiso  10800  seq3coll  10803  caucvgrelemrec  10969  resqrexlemex  11015  minmax  11219  xrminmax  11254  fsum2dlemstep  11423  fisumcom2  11427  zproddc  11568  fprod2dlemstep  11611  fprodcom2fi  11615  zsupcllemstep  11926  zsupssdc  11935  bezoutlemmain  11979  sqgcd  12010  pcpremul  12273  pceulem  12274  pceu  12275  pczpre  12277  pcdiv  12282  pcqmul  12283  pcqdiv  12287  pcexp  12289  pcdvdsb  12299  pcneg  12304  pcdvdstr  12306  pcgcd1  12307  pc2dvds  12309  pcz  12311  pcaddlem  12318  pcadd  12319  qexpz  12330  expnprm  12331  infpnlem2  12338  mndpropd  12730  grpsubpropd2  12861  ablnnncan  12950  ringpropd  13040  neiint  13309  restbasg  13332  iscnp4  13382  cnconst2  13397  cnpdis  13406  neitx  13432  upxp  13436  hmeoimaf1o  13478  blssexps  13593  blssex  13594  ssblex  13595  bdmopn  13668  xmettx  13674  metcnp3  13675  tgioo  13710  tgqioo  13711  sin0pilem2  13867  logbgcd1irr  14049  lgsval  14069  lgsfcl2  14071  lgsdir  14100  lgsdilem2  14101  lgsdi  14102  lgsne0  14103  pwle2  14401
  Copyright terms: Public domain W3C validator