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

Theorem syl22anc 1202
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 1199 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  5379  tfrexlem  6199  th3qlem1  6499  enpr2d  6679  ssenen  6713  phplem4dom  6724  phplem4on  6729  fiunsnnn  6743  findcard2sd  6754  unsnfi  6775  sbthlemi9  6821  endjusym  6949  endjudisj  7034  djuen  7035  ltanqg  7176  ltmnqg  7177  ltnnnq  7199  addcmpblnq0  7219  addlocprlemeqgt  7308  distrlem1prl  7358  distrlem1pru  7359  distrlem4prl  7360  distrlem4pru  7361  addcanprleml  7390  recexprlem1ssl  7409  caucvgprlemloc  7451  caucvgprprlemloccalc  7460  mulcmpblnr  7517  ltasrg  7546  recexgt0sr  7549  mulextsr1lem  7556  mulextsr1  7557  srpospr  7559  prsrlt  7563  ltpsrprg  7579  mappsrprg  7580  pitonnlem1p1  7622  recidpirq  7634  axpre-ltadd  7662  mulgt0d  7853  mul4d  7885  add4d  7899  add42d  7900  subcan  7985  addsub4d  8088  subadd4d  8089  sub4d  8090  2addsubd  8091  addsubeq4d  8092  muladdd  8146  mulsubd  8147  addgegt0d  8249  addge0d  8251  le2addd  8292  le2subd  8293  ltleaddd  8294  leltaddd  8295  lt2subd  8297  apreap  8316  apsym  8335  apcotr  8336  apadd1  8337  apneg  8340  mulext1  8341  mulap0r  8344  mulge0d  8350  mulap0d  8386  divdivdivap  8440  divcanap5  8441  divap0d  8533  recdivapd  8534  recdivap2d  8535  divcanap6d  8536  ddcanapd  8537  rec11apd  8538  divmuldivapd  8559  prodgt0  8574  lt2msq  8608  ledivdiv  8612  lediv12a  8616  recreclt  8622  divgt0d  8657  mulgt1d  8658  lemulge11d  8659  lemulge12d  8660  ltmul12ad  8663  lemul12ad  8664  lemul12bd  8665  nndivtr  8726  qreccl  9390  ledivdivd  9464  lediv12ad  9498  lt2mul2divd  9507  xlt2add  9618  xleaddadd  9625  iccss2  9682  iccssico2  9685  lincmb01cmp  9741  iccf1o  9742  fzrev2i  9821  qtri3or  9975  2tnp1ge0ge0  10029  modqid  10077  q0mod  10083  q1mod  10084  modqabs  10085  modqadd1  10089  mulqaddmodid  10092  mulp1mod1  10093  modqmuladd  10094  modqmuladdnn0  10096  qnegmod  10097  m1modnnsub1  10098  addmodid  10100  modqm1p1mod0  10103  modqltm1p1mod  10104  modqmul1  10105  q2submod  10113  modifeq2int  10114  modaddmodup  10115  modaddmodlo  10116  modqaddmulmod  10119  modqsubdir  10121  modqeqmodmin  10122  modsumfzodifsn  10124  addmodlteq  10126  frecfzennn  10154  ser3mono  10206  expcl2lemap  10260  mulexpzap  10288  expaddzaplem  10291  expaddzap  10292  expmulzap  10294  ltexp2a  10300  leexp2a  10301  sqdivap  10312  expnbnd  10370  expsubapd  10390  lt2sqd  10410  le2sqd  10411  sq11d  10412  bcp1nk  10463  hashunlem  10505  zfz1isolem1  10538  cjap  10633  cnreim  10705  resqrexlem1arp  10732  resqrexlemp1rp  10733  resqrexlemglsq  10749  abs00ap  10789  absext  10790  absexpzap  10807  absrele  10810  sqrtmuld  10896  sqrtsq2d  10897  sqrtled  10898  sqrtltd  10899  sqr11d  10900  abs3lemd  10928  minmax  10956  xrmaxiflemlub  10972  xrltmaxsup  10981  xrminmax  10989  xrbdtri  11000  climuni  11017  2clim  11025  addcn2  11034  mulcn2  11036  fsum3  11111  mptfzshft  11166  fsumrev  11167  fisum0diag2  11171  modfsummodlemstep  11181  binomlem  11207  mertenslemi1  11259  efcllemp  11278  dvds1  11463  dvdsext  11465  mulmoddvds  11473  oexpneg  11486  evennn02n  11491  evennn2n  11492  bezoutlemmo  11606  mulgcd  11616  dvdssqlem  11630  rpmulgcd2  11688  isprm6  11737  sqrt2irraplemnn  11768  sqrt2irrap  11769  crth  11811  unennn  11821  ennnfonelemg  11827  ennnfonelemhf1o  11837  inffinp1  11853  isstructr  11885  ntrin  12204  topssnei  12242  restbasg  12248  cnntri  12304  txcn  12355  txlm  12359  cnmpt2res  12377  psmetlecl  12414  xmetlecl  12447  bldisj  12481  bdmet  12582  bdbl  12583  bdmopn  12584  xmetxp  12587  metcnp  12592  tgioo  12626  cncfmet  12659  dedekindeulemlub  12678  suplociccreex  12682  ellimc3apf  12709  limcimolemlt  12713  limccnp2cntop  12726  dvfvalap  12730  dvmulxxbr  12746  dvaddxx  12747  dvmulxx  12748  dviaddf  12749  dvimulf  12750  dvcoapbr  12751  dvmptclx  12760
  Copyright terms: Public domain W3C validator