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

Theorem syl22anc 1217
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 1214 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  5411  tfrexlem  6231  th3qlem1  6531  enpr2d  6711  ssenen  6745  phplem4dom  6756  phplem4on  6761  fiunsnnn  6775  findcard2sd  6786  unsnfi  6807  sbthlemi9  6853  endjusym  6981  endjudisj  7073  djuen  7074  ltanqg  7222  ltmnqg  7223  ltnnnq  7245  addcmpblnq0  7265  addlocprlemeqgt  7354  distrlem1prl  7404  distrlem1pru  7405  distrlem4prl  7406  distrlem4pru  7407  addcanprleml  7436  recexprlem1ssl  7455  caucvgprlemloc  7497  caucvgprprlemloccalc  7506  mulcmpblnr  7563  ltasrg  7592  recexgt0sr  7595  mulextsr1lem  7602  mulextsr1  7603  srpospr  7605  prsrlt  7609  ltpsrprg  7625  mappsrprg  7626  pitonnlem1p1  7668  recidpirq  7680  axpre-ltadd  7708  mulgt0d  7899  mul4d  7931  add4d  7945  add42d  7946  subcan  8031  addsub4d  8134  subadd4d  8135  sub4d  8136  2addsubd  8137  addsubeq4d  8138  muladdd  8192  mulsubd  8193  addgegt0d  8295  addgtge0d  8296  addge0d  8298  le2addd  8339  le2subd  8340  ltleaddd  8341  leltaddd  8342  lt2subd  8344  apreap  8363  apsym  8382  apcotr  8383  apadd1  8384  apneg  8387  mulext1  8388  mulap0r  8391  mulge0d  8397  mulap0d  8433  divdivdivap  8487  divcanap5  8488  divap0d  8580  recdivapd  8581  recdivap2d  8582  divcanap6d  8583  ddcanapd  8584  rec11apd  8585  divmuldivapd  8606  subrecapd  8614  prodgt0  8624  lt2msq  8658  ledivdiv  8662  lediv12a  8666  recreclt  8672  divgt0d  8707  mulgt1d  8708  lemulge11d  8709  lemulge12d  8710  ltmul12ad  8713  lemul12ad  8714  lemul12bd  8715  nndivtr  8776  qreccl  9448  ledivdivd  9523  lediv12ad  9557  lt2mul2divd  9566  xlt2add  9677  xleaddadd  9684  iccss2  9741  iccssico2  9744  lincmb01cmp  9800  iccf1o  9801  fzrev2i  9880  qtri3or  10034  2tnp1ge0ge0  10088  modqid  10136  q0mod  10142  q1mod  10143  modqabs  10144  modqadd1  10148  mulqaddmodid  10151  mulp1mod1  10152  modqmuladd  10153  modqmuladdnn0  10155  qnegmod  10156  m1modnnsub1  10157  addmodid  10159  modqm1p1mod0  10162  modqltm1p1mod  10163  modqmul1  10164  q2submod  10172  modifeq2int  10173  modaddmodup  10174  modaddmodlo  10175  modqaddmulmod  10178  modqsubdir  10180  modqeqmodmin  10181  modsumfzodifsn  10183  addmodlteq  10185  frecfzennn  10213  ser3mono  10265  expcl2lemap  10319  mulexpzap  10347  expaddzaplem  10350  expaddzap  10351  expmulzap  10353  ltexp2a  10359  leexp2a  10360  sqdivap  10371  expnbnd  10429  expsubapd  10449  lt2sqd  10469  le2sqd  10470  sq11d  10471  bcp1nk  10522  hashunlem  10564  zfz1isolem1  10597  cjap  10692  cnreim  10764  resqrexlem1arp  10791  resqrexlemp1rp  10792  resqrexlemglsq  10808  abs00ap  10848  absext  10849  absexpzap  10866  absrele  10869  sqrtmuld  10955  sqrtsq2d  10956  sqrtled  10957  sqrtltd  10958  sqr11d  10959  abs3lemd  10987  minmax  11015  xrmaxiflemlub  11031  xrltmaxsup  11040  xrminmax  11048  xrbdtri  11059  climuni  11076  2clim  11084  addcn2  11093  mulcn2  11095  fsum3  11170  mptfzshft  11225  fsumrev  11226  fisum0diag2  11230  modfsummodlemstep  11240  binomlem  11266  mertenslemi1  11318  efcllemp  11378  dvds1  11564  dvdsext  11566  mulmoddvds  11574  oexpneg  11587  evennn02n  11592  evennn2n  11593  bezoutlemmo  11707  mulgcd  11717  dvdssqlem  11731  rpmulgcd2  11789  isprm6  11838  sqrt2irraplemnn  11870  sqrt2irrap  11871  crth  11913  unennn  11923  ennnfonelemg  11929  ennnfonelemhf1o  11939  inffinp1  11955  isstructr  11990  ntrin  12309  topssnei  12347  restbasg  12353  cnntri  12409  txcn  12460  txlm  12464  cnmpt2res  12482  psmetlecl  12519  xmetlecl  12552  bldisj  12586  bdmet  12687  bdbl  12688  bdmopn  12689  xmetxp  12692  metcnp  12697  tgioo  12731  cncfmet  12764  dedekindeulemlub  12783  suplociccreex  12787  ellimc3apf  12814  limcimolemlt  12818  limccnp2cntop  12831  dvfvalap  12835  dvmulxxbr  12851  dvaddxx  12852  dvmulxx  12853  dviaddf  12854  dvimulf  12855  dvcoapbr  12856  dvmptclx  12865  cxplt3  13021  cxpltd  13029  cxpled  13030  cxplt3d  13035  cxple3d  13036
  Copyright terms: Public domain W3C validator