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

Theorem syl22anc 1171
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 300 . 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 1168 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  f1oprg  5193  tfrexlem  5977  th3qlem1  6267  phplem4dom  6387  phplem4on  6392  fiunsnnn  6405  findcard2sd  6416  unsnfi  6429  ltanqg  6641  ltmnqg  6642  ltnnnq  6664  addcmpblnq0  6684  addlocprlemeqgt  6773  distrlem1prl  6823  distrlem1pru  6824  distrlem4prl  6825  distrlem4pru  6826  addcanprleml  6855  recexprlem1ssl  6874  caucvgprlemloc  6916  caucvgprprlemloccalc  6925  mulcmpblnr  6969  ltasrg  6998  recexgt0sr  7001  mulextsr1lem  7007  mulextsr1  7008  srpospr  7010  prsrlt  7014  pitonnlem1p1  7065  recidpirq  7077  axpre-ltadd  7103  mulgt0d  7288  mul4d  7319  add4d  7333  add42d  7334  subcan  7419  addsub4d  7522  subadd4d  7523  sub4d  7524  2addsubd  7525  addsubeq4d  7526  muladdd  7576  mulsubd  7577  addgegt0d  7676  addge0d  7678  le2addd  7719  le2subd  7720  ltleaddd  7721  leltaddd  7722  lt2subd  7724  apreap  7743  apsym  7762  apcotr  7763  apadd1  7764  apneg  7767  mulext1  7768  mulap0r  7771  mulge0d  7777  mulap0d  7804  divdivdivap  7857  divcanap5  7858  divap0d  7949  recdivapd  7950  recdivap2d  7951  divcanap6d  7952  ddcanapd  7953  rec11apd  7954  divmuldivapd  7974  prodgt0  7986  lt2msq  8020  ledivdiv  8024  lediv12a  8028  recreclt  8034  divgt0d  8069  mulgt1d  8070  lemulge11d  8071  lemulge12d  8072  ltmul12ad  8075  lemul12ad  8076  lemul12bd  8077  nndivtr  8136  qreccl  8797  ledivdivd  8869  lediv12ad  8903  lt2mul2divd  8906  iccss2  9032  iccssico2  9035  lincmb01cmp  9090  iccf1o  9091  fzrev2i  9168  qtri3or  9318  2tnp1ge0ge0  9372  modqid  9420  q0mod  9426  q1mod  9427  modqabs  9428  modqadd1  9432  mulqaddmodid  9435  mulp1mod1  9436  modqmuladd  9437  modqmuladdnn0  9439  qnegmod  9440  m1modnnsub1  9441  addmodid  9443  modqm1p1mod0  9446  modqltm1p1mod  9447  modqmul1  9448  q2submod  9456  modifeq2int  9457  modaddmodup  9458  modaddmodlo  9459  modqaddmulmod  9462  modqsubdir  9464  modqeqmodmin  9465  modsumfzodifsn  9467  addmodlteq  9469  frecfzennn  9497  isermono  9542  expcl2lemap  9574  mulexpzap  9602  expaddzaplem  9605  expaddzap  9606  expmulzap  9608  ltexp2a  9614  leexp2a  9615  sqdivap  9626  expnbnd  9682  expsubapd  9702  lt2sqd  9722  le2sqd  9723  sq11d  9724  bcp1nk  9775  sizeunlem  9817  cjap  9920  resqrexlem1arp  10018  resqrexlemp1rp  10019  resqrexlemglsq  10035  abs00ap  10075  absext  10076  absexpzap  10093  absrele  10096  sqrtmuld  10182  sqrtsq2d  10183  sqrtled  10184  sqrtltd  10185  sqr11d  10186  abs3lemd  10214  minmax  10239  climuni  10259  2clim  10267  addcn2  10276  mulcn2  10278  dvds1  10387  dvdsext  10389  mulmoddvds  10397  oexpneg  10410  evennn02n  10415  evennn2n  10416  bezoutlemmo  10528  mulgcd  10538  dvdssqlem  10552  rpmulgcd2  10610  isprm6  10659  sqrt2irraplemnn  10690  sqrt2irrap  10691
  Copyright terms: Public domain W3C validator