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

Theorem syl22anc 1239
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 306 . 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 1236 1  |-  ( ph  ->  et )
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:  f1oprg  5497  tfrexlem  6325  th3qlem1  6627  enpr2d  6807  ssenen  6841  phplem4dom  6852  phplem4on  6857  fiunsnnn  6871  findcard2sd  6882  unsnfi  6908  sbthlemi9  6954  endjusym  7085  endjudisj  7199  djuen  7200  ltanqg  7374  ltmnqg  7375  ltnnnq  7397  addcmpblnq0  7417  addlocprlemeqgt  7506  distrlem1prl  7556  distrlem1pru  7557  distrlem4prl  7558  distrlem4pru  7559  addcanprleml  7588  recexprlem1ssl  7607  caucvgprlemloc  7649  caucvgprprlemloccalc  7658  mulcmpblnr  7715  ltasrg  7744  recexgt0sr  7747  mulextsr1lem  7754  mulextsr1  7755  srpospr  7757  prsrlt  7761  ltpsrprg  7777  mappsrprg  7778  pitonnlem1p1  7820  recidpirq  7832  axpre-ltadd  7860  mulgt0d  8054  mul4d  8086  add4d  8100  add42d  8101  subcan  8186  addsub4d  8289  subadd4d  8290  sub4d  8291  2addsubd  8292  addsubeq4d  8293  muladdd  8347  mulsubd  8348  addgegt0d  8450  addgtge0d  8451  addge0d  8453  le2addd  8494  le2subd  8495  ltleaddd  8496  leltaddd  8497  lt2subd  8499  apreap  8518  apsym  8537  apcotr  8538  apadd1  8539  apneg  8542  mulext1  8543  mulap0r  8546  mulge0d  8552  mulap0d  8588  divdivdivap  8642  divcanap5  8643  divap0d  8735  recdivapd  8736  recdivap2d  8737  divcanap6d  8738  ddcanapd  8739  rec11apd  8740  divmuldivapd  8761  divmuleqapd  8762  subrecapd  8770  prodgt0  8780  lt2msq  8814  ledivdiv  8818  lediv12a  8822  recreclt  8828  divgt0d  8863  mulgt1d  8864  lemulge11d  8865  lemulge12d  8866  ltmul12ad  8869  lemul12ad  8870  lemul12bd  8871  nndivtr  8932  qreccl  9613  ledivdivd  9691  lediv12ad  9725  lt2mul2divd  9734  xlt2add  9849  xleaddadd  9856  iccss2  9913  iccssico2  9916  lincmb01cmp  9972  iccf1o  9973  fzrev2i  10054  qtri3or  10211  elicore  10235  2tnp1ge0ge0  10269  modqid  10317  q0mod  10323  q1mod  10324  modqabs  10325  modqadd1  10329  mulqaddmodid  10332  mulp1mod1  10333  modqmuladd  10334  modqmuladdnn0  10336  qnegmod  10337  m1modnnsub1  10338  addmodid  10340  modqm1p1mod0  10343  modqltm1p1mod  10344  modqmul1  10345  q2submod  10353  modifeq2int  10354  modaddmodup  10355  modaddmodlo  10356  modqaddmulmod  10359  modqsubdir  10361  modqeqmodmin  10362  modsumfzodifsn  10364  addmodlteq  10366  frecfzennn  10394  ser3mono  10446  expcl2lemap  10500  mulexpzap  10528  expaddzaplem  10531  expaddzap  10532  expmulzap  10534  ltexp2a  10540  leexp2a  10541  sqdivap  10552  qsqeqor  10598  expnbnd  10611  expsubapd  10632  lt2sqd  10652  le2sqd  10653  sq11d  10654  apexp1  10664  bcp1nk  10708  hashunlem  10751  zfz1isolem1  10787  cjap  10882  cnreim  10954  resqrexlem1arp  10981  resqrexlemp1rp  10982  resqrexlemglsq  10998  abs00ap  11038  absext  11039  absexpzap  11056  absrele  11059  sqrtmuld  11145  sqrtsq2d  11146  sqrtled  11147  sqrtltd  11148  sqr11d  11149  abs3lemd  11177  minmax  11205  xrmaxiflemlub  11223  xrltmaxsup  11232  xrminmax  11240  xrbdtri  11251  climuni  11268  2clim  11276  addcn2  11285  mulcn2  11287  fsum3  11362  mptfzshft  11417  fsumrev  11418  fisum0diag2  11422  modfsummodlemstep  11432  binomlem  11458  mertenslemi1  11510  fprodrev  11594  efcllemp  11633  p1modz1  11768  dvds1  11825  dvdsext  11827  mulmoddvds  11835  oexpneg  11848  evennn02n  11853  evennn2n  11854  bezoutlemmo  11973  mulgcd  11983  dvdssqlem  11997  rpmulgcd2  12061  isprm6  12113  sqrt2irraplemnn  12145  sqrt2irrap  12146  crth  12190  eulerthlemh  12197  prmdiveq  12202  powm2modprm  12218  modprm0  12220  pythagtriplem2  12232  pythagtriplem11  12240  pythagtriplem13  12242  pythagtrip  12249  pcid  12289  pcgcd1  12293  pcprmpw2  12298  dvdsprmpweqle  12302  pcaddlem  12304  pcadd  12305  fldivp1  12312  unennn  12364  ennnfonelemg  12370  ennnfonelemhf1o  12380  inffinp1  12396  isstructr  12443  ntrin  13117  topssnei  13155  restbasg  13161  cnntri  13217  txcn  13268  txlm  13272  cnmpt2res  13290  psmetlecl  13327  xmetlecl  13360  bldisj  13394  bdmet  13495  bdbl  13496  bdmopn  13497  xmetxp  13500  metcnp  13505  tgioo  13539  cncfmet  13572  dedekindeulemlub  13591  suplociccreex  13595  ellimc3apf  13622  limcimolemlt  13626  limccnp2cntop  13639  dvfvalap  13643  dvmulxxbr  13659  dvaddxx  13660  dvmulxx  13661  dviaddf  13662  dvimulf  13663  dvcoapbr  13664  dvmptclx  13673  cxplt3  13833  cxpltd  13841  cxpled  13842  cxplt3d  13847  cxple3d  13848  logbrec  13871  logbgcd1irraplemap  13880  lgslem1  13894  lgslem3  13896  lgsdirprm  13928  2sqlem7  13950
  Copyright terms: Public domain W3C validator