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

Theorem syl22anc 1228
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
syl22anc.5  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta ) )  ->  et )
Assertion
Ref Expression
syl22anc  |-  ( ph  ->  et )

Proof of Theorem syl22anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 304 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylXanc.3 . 2  |-  ( ph  ->  th )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl22anc.5 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta ) )  ->  et )
73, 4, 5, 6syl12anc 1225 1  |-  ( ph  ->  et )
Colors of variables: wff set class
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:  f1oprg  5471  tfrexlem  6294  th3qlem1  6595  enpr2d  6775  ssenen  6809  phplem4dom  6820  phplem4on  6825  fiunsnnn  6839  findcard2sd  6850  unsnfi  6876  sbthlemi9  6922  endjusym  7053  endjudisj  7158  djuen  7159  ltanqg  7333  ltmnqg  7334  ltnnnq  7356  addcmpblnq0  7376  addlocprlemeqgt  7465  distrlem1prl  7515  distrlem1pru  7516  distrlem4prl  7517  distrlem4pru  7518  addcanprleml  7547  recexprlem1ssl  7566  caucvgprlemloc  7608  caucvgprprlemloccalc  7617  mulcmpblnr  7674  ltasrg  7703  recexgt0sr  7706  mulextsr1lem  7713  mulextsr1  7714  srpospr  7716  prsrlt  7720  ltpsrprg  7736  mappsrprg  7737  pitonnlem1p1  7779  recidpirq  7791  axpre-ltadd  7819  mulgt0d  8013  mul4d  8045  add4d  8059  add42d  8060  subcan  8145  addsub4d  8248  subadd4d  8249  sub4d  8250  2addsubd  8251  addsubeq4d  8252  muladdd  8306  mulsubd  8307  addgegt0d  8409  addgtge0d  8410  addge0d  8412  le2addd  8453  le2subd  8454  ltleaddd  8455  leltaddd  8456  lt2subd  8458  apreap  8477  apsym  8496  apcotr  8497  apadd1  8498  apneg  8501  mulext1  8502  mulap0r  8505  mulge0d  8511  mulap0d  8547  divdivdivap  8601  divcanap5  8602  divap0d  8694  recdivapd  8695  recdivap2d  8696  divcanap6d  8697  ddcanapd  8698  rec11apd  8699  divmuldivapd  8720  divmuleqapd  8721  subrecapd  8729  prodgt0  8739  lt2msq  8773  ledivdiv  8777  lediv12a  8781  recreclt  8787  divgt0d  8822  mulgt1d  8823  lemulge11d  8824  lemulge12d  8825  ltmul12ad  8828  lemul12ad  8829  lemul12bd  8830  nndivtr  8891  qreccl  9572  ledivdivd  9650  lediv12ad  9684  lt2mul2divd  9693  xlt2add  9808  xleaddadd  9815  iccss2  9872  iccssico2  9875  lincmb01cmp  9931  iccf1o  9932  fzrev2i  10012  qtri3or  10169  elicore  10193  2tnp1ge0ge0  10227  modqid  10275  q0mod  10281  q1mod  10282  modqabs  10283  modqadd1  10287  mulqaddmodid  10290  mulp1mod1  10291  modqmuladd  10292  modqmuladdnn0  10294  qnegmod  10295  m1modnnsub1  10296  addmodid  10298  modqm1p1mod0  10301  modqltm1p1mod  10302  modqmul1  10303  q2submod  10311  modifeq2int  10312  modaddmodup  10313  modaddmodlo  10314  modqaddmulmod  10317  modqsubdir  10319  modqeqmodmin  10320  modsumfzodifsn  10322  addmodlteq  10324  frecfzennn  10352  ser3mono  10404  expcl2lemap  10458  mulexpzap  10486  expaddzaplem  10489  expaddzap  10490  expmulzap  10492  ltexp2a  10498  leexp2a  10499  sqdivap  10510  expnbnd  10568  expsubapd  10589  lt2sqd  10609  le2sqd  10610  sq11d  10611  apexp1  10621  bcp1nk  10665  hashunlem  10707  zfz1isolem1  10743  cjap  10838  cnreim  10910  resqrexlem1arp  10937  resqrexlemp1rp  10938  resqrexlemglsq  10954  abs00ap  10994  absext  10995  absexpzap  11012  absrele  11015  sqrtmuld  11101  sqrtsq2d  11102  sqrtled  11103  sqrtltd  11104  sqr11d  11105  abs3lemd  11133  minmax  11161  xrmaxiflemlub  11179  xrltmaxsup  11188  xrminmax  11196  xrbdtri  11207  climuni  11224  2clim  11232  addcn2  11241  mulcn2  11243  fsum3  11318  mptfzshft  11373  fsumrev  11374  fisum0diag2  11378  modfsummodlemstep  11388  binomlem  11414  mertenslemi1  11466  fprodrev  11550  efcllemp  11589  p1modz1  11724  dvds1  11780  dvdsext  11782  mulmoddvds  11790  oexpneg  11803  evennn02n  11808  evennn2n  11809  bezoutlemmo  11928  mulgcd  11938  dvdssqlem  11952  rpmulgcd2  12016  isprm6  12068  sqrt2irraplemnn  12100  sqrt2irrap  12101  crth  12145  eulerthlemh  12152  prmdiveq  12157  powm2modprm  12173  modprm0  12175  pythagtriplem2  12187  pythagtriplem11  12195  pythagtriplem13  12197  pythagtrip  12204  pcid  12244  pcgcd1  12248  pcprmpw2  12253  dvdsprmpweqle  12257  pcaddlem  12259  pcadd  12260  fldivp1  12267  unennn  12293  ennnfonelemg  12299  ennnfonelemhf1o  12309  inffinp1  12325  isstructr  12372  ntrin  12691  topssnei  12729  restbasg  12735  cnntri  12791  txcn  12842  txlm  12846  cnmpt2res  12864  psmetlecl  12901  xmetlecl  12934  bldisj  12968  bdmet  13069  bdbl  13070  bdmopn  13071  xmetxp  13074  metcnp  13079  tgioo  13113  cncfmet  13146  dedekindeulemlub  13165  suplociccreex  13169  ellimc3apf  13196  limcimolemlt  13200  limccnp2cntop  13213  dvfvalap  13217  dvmulxxbr  13233  dvaddxx  13234  dvmulxx  13235  dviaddf  13236  dvimulf  13237  dvcoapbr  13238  dvmptclx  13247  cxplt3  13407  cxpltd  13415  cxpled  13416  cxplt3d  13421  cxple3d  13422  logbrec  13445  logbgcd1irraplemap  13454
  Copyright terms: Public domain W3C validator