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

Theorem 3ad2ant1 964
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
3ad2ant1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )

Proof of Theorem 3ad2ant1
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantr 270 . 2  |-  ( (
ph  /\  th )  ->  ch )
323adant2 962 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  simp1l  967  simp1r  968  simp11  973  simp12  974  simp13  975  simp1ll  1006  simp1lr  1007  simp1rl  1008  simp1rr  1009  simp1l1  1036  simp1l2  1037  simp1l3  1038  simp1r1  1039  simp1r2  1040  simp1r3  1041  simp11l  1054  simp11r  1055  simp12l  1056  simp12r  1057  simp13l  1058  simp13r  1059  simp111  1072  simp112  1073  simp113  1074  simp121  1075  simp122  1076  simp123  1077  simp131  1078  simp132  1079  simp133  1080  3anim123i  1128  3jaao  1244  ceqsalt  2645  sbciegft  2867  reupick2  3283  ifbothdc  3419  frirrg  4168  breldmg  4630  fntpg  5056  funimaexglem  5083  fex2  5164  fvun1  5354  fprg  5464  fsnunfv  5481  fnfvima  5511  cocan1  5548  cocan2  5549  mpt2fvex  5955  poxp  5979  smoiso  6049  tfrlem5  6061  tfrlemibxssdm  6074  tfr1onlembfn  6091  tfri1dALT  6098  tfrcllembfn  6104  rdgon  6133  freccllem  6149  nnawordex  6267  mapxpen  6544  fidceq  6565  fidifsnen  6566  dif1en  6575  en2eqpr  6603  unsnfi  6609  unsnfidcex  6610  unsnfidcel  6611  fisseneq  6621  ordiso2  6707  updjud  6752  mulcanenq0ec  6983  prltlu  7025  prarloclem3step  7034  prarloclem5  7038  ltasrg  7295  cnegexlem1  7636  addcan  7641  apcotr  8060  apadd1  8061  mulext1  8065  divdivap1  8164  divdivap2  8165  div2negap  8176  divneg2ap  8177  ltmulgt11  8297  ltdiv2  8320  squeeze0  8337  nndivtr  8435  nn0n0n1ge2  8787  zdivmul  8806  gtndiv  8811  eluzuzle  8996  eluzp1p1  9013  qdivcl  9097  irrmul  9101  rpgecl  9131  lbico1  9317  lbicc2  9370  zltaddlt1le  9392  uzsubsubfz  9430  elfz1b  9471  elfz0ubfz0  9501  fz0fzelfz0  9503  difelfzle  9510  difelfznle  9511  2ffzeq  9517  fzo1fzo0n0  9559  ubmelfzo  9576  fzonn0p1p1  9589  elfzom1p1elfzo  9590  elfzonelfzo  9606  subfzo0  9618  ceiqle  9685  ceilqle  9686  modqval  9696  flqpmodeq  9699  modq0  9701  negqmod0  9703  modqge0  9704  modqlt  9705  modqdiffl  9707  modqmulnn  9714  modqvalp1  9715  modqmuladdnn0  9740  qnegmod  9741  addmodid  9744  modfzo0difsn  9767  addmodlteq  9770  qexpclz  9941  expgt1  9958  expp1zap  9969  expm1ap  9970  expubnd  9977  bernneq2  10040  expnlbnd  10043  omgadd  10175  hashun  10178  fihashssdif  10191  hashdifpr  10193  fimaxq  10200  shftuz  10216  mulreap  10263  redivap  10273  imdivap  10280  resqrtcl  10427  climuni  10645  addcn2  10663  mulcn2  10665  dvdsval2  10892  addmodlteqALT  10953  modremain  11022  fldivndvdslt  11028  mulgcdr  11100  gcddiv  11101  rpmulgcd  11108  rplpwr  11109  rppwr  11110  qredeq  11171  divgcdcoprmex  11177  cncongr1  11178  cncongr2  11179  dvdsnprmd  11200  euclemma  11218  prmexpb  11223  qnumdenbi  11263  hashgcdlem  11296  unennn  11303  bdfind  11498
  Copyright terms: Public domain W3C validator