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

Theorem syl22anc 1145
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 294 . 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 1142 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  f1oprg  5193  tfrexlem  5976  th3qlem1  6236  phplem4dom  6352  phplem4on  6357  fiunsnnn  6366  findcard2sd  6377  ltanqg  6526  ltmnqg  6527  ltnnnq  6549  addcmpblnq0  6569  addlocprlemeqgt  6658  distrlem1prl  6708  distrlem1pru  6709  distrlem4prl  6710  distrlem4pru  6711  addcanprleml  6740  recexprlem1ssl  6759  caucvgprlemloc  6801  caucvgprprlemloccalc  6810  mulcmpblnr  6854  ltasrg  6883  recexgt0sr  6886  mulextsr1lem  6892  mulextsr1  6893  srpospr  6895  prsrlt  6899  pitonnlem1p1  6950  recidpirq  6962  axpre-ltadd  6988  mulgt0d  7168  mul4d  7199  add4d  7213  add42d  7214  subcan  7299  addsub4d  7402  subadd4d  7403  sub4d  7404  2addsubd  7405  addsubeq4d  7406  muladdd  7455  mulsubd  7456  addgegt0d  7555  addge0d  7557  le2addd  7598  le2subd  7599  ltleaddd  7600  leltaddd  7601  lt2subd  7603  apreap  7622  apsym  7641  apcotr  7642  apadd1  7643  apneg  7646  mulext1  7647  mulap0r  7650  mulge0d  7656  mulap0d  7683  divdivdivap  7734  divcanap5  7735  divap0d  7826  recdivapd  7827  recdivap2d  7828  divcanap6d  7829  ddcanapd  7830  rec11apd  7831  divmuldivapd  7851  prodgt0  7863  lt2msq  7897  ledivdiv  7901  lediv12a  7905  recreclt  7911  divgt0d  7946  mulgt1d  7947  lemulge11d  7948  lemulge12d  7949  ltmul12ad  7952  lemul12ad  7953  lemul12bd  7954  nndivtr  8001  qreccl  8644  ledivdivd  8716  lediv12ad  8750  lt2mul2divd  8753  iccss2  8884  iccssico2  8887  lincmb01cmp  8942  iccf1o  8943  fzrev2i  9020  qtri3or  9170  2tnp1ge0ge0  9216  modqid  9264  q0mod  9270  q1mod  9271  modqabs  9272  modqadd1  9276  mulqaddmodid  9279  mulp1mod1  9280  modqmuladd  9281  modqmuladdnn0  9283  qnegmod  9284  m1modnnsub1  9285  addmodid  9287  modqm1p1mod0  9290  modqltm1p1mod  9291  modqmul1  9292  q2submod  9300  modifeq2int  9301  modaddmodup  9302  modaddmodlo  9303  modqaddmulmod  9306  modqsubdir  9308  modqeqmodmin  9309  modsumfzodifsn  9311  addmodlteq  9313  frecfzennn  9332  isermono  9366  expcl2lemap  9397  mulexpzap  9425  expaddzaplem  9428  expaddzap  9429  expmulzap  9431  ltexp2a  9437  leexp2a  9438  sqdivap  9449  expnbnd  9504  expsubapd  9524  lt2sqd  9544  le2sqd  9545  sq11d  9546  bcp1nk  9594  cjap  9698  resqrexlem1arp  9795  resqrexlemp1rp  9796  resqrexlemglsq  9812  abs00ap  9852  absext  9853  absexpzap  9870  absrele  9873  sqrtmuld  9959  sqrtsq2d  9960  sqrtled  9961  sqrtltd  9962  sqr11d  9963  abs3lemd  9991  climuni  10008  2clim  10016  addcn2  10025  mulcn2  10027  dvds1  10128  dvdsext  10130  mulmoddvds  10138  oexpneg  10151  evennn02n  10157  evennn2n  10158
  Copyright terms: Public domain W3C validator