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

Theorem 3ad2ant1 960
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 958 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 920
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 922
This theorem is referenced by:  simp1l  963  simp1r  964  simp11  969  simp12  970  simp13  971  simp1ll  1002  simp1lr  1003  simp1rl  1004  simp1rr  1005  simp1l1  1032  simp1l2  1033  simp1l3  1034  simp1r1  1035  simp1r2  1036  simp1r3  1037  simp11l  1050  simp11r  1051  simp12l  1052  simp12r  1053  simp13l  1054  simp13r  1055  simp111  1068  simp112  1069  simp113  1070  simp121  1071  simp122  1072  simp123  1073  simp131  1074  simp132  1075  simp133  1076  3anim123i  1124  3jaao  1240  ceqsalt  2634  sbciegft  2853  reupick2  3266  ifbothdc  3398  frirrg  4133  breldmg  4589  fntpg  5006  funimaexglem  5033  fex2  5110  fvun1  5291  fprg  5398  fsnunfv  5415  fnfvima  5445  cocan1  5478  cocan2  5479  mpt2fvex  5880  poxp  5904  smoiso  5971  tfrlem5  5983  tfrlemibxssdm  5996  tfr1onlembfn  6013  tfri1dALT  6020  tfrcllembfn  6026  rdgon  6055  freccllem  6071  nnawordex  6188  fidceq  6425  fidifsnen  6426  dif1en  6435  en2eqpr  6458  unsnfi  6463  unsnfidcex  6464  unsnfidcel  6465  fisseneq  6474  ordiso2  6540  mulcanenq0ec  6749  prltlu  6791  prarloclem3step  6800  prarloclem5  6804  ltasrg  7061  cnegexlem1  7402  addcan  7407  apcotr  7826  apadd1  7827  mulext1  7831  divdivap1  7930  divdivap2  7931  div2negap  7942  divneg2ap  7943  ltmulgt11  8061  ltdiv2  8084  squeeze0  8101  nndivtr  8199  nn0n0n1ge2  8551  zdivmul  8570  gtndiv  8575  eluzuzle  8760  eluzp1p1  8777  qdivcl  8861  irrmul  8865  rpgecl  8895  lbico1  9081  lbicc2  9134  zltaddlt1le  9156  uzsubsubfz  9194  elfz1b  9235  elfz0ubfz0  9265  fz0fzelfz0  9267  difelfzle  9274  difelfznle  9275  2ffzeq  9280  fzo1fzo0n0  9321  ubmelfzo  9338  fzonn0p1p1  9351  elfzom1p1elfzo  9352  elfzonelfzo  9368  subfzo0  9380  ceiqle  9447  ceilqle  9448  modqval  9458  flqpmodeq  9461  modq0  9463  negqmod0  9465  modqge0  9466  modqlt  9467  modqdiffl  9469  modqmulnn  9476  modqvalp1  9477  modqmuladdnn0  9502  qnegmod  9503  addmodid  9506  modfzo0difsn  9529  addmodlteq  9532  qexpclz  9646  expgt1  9663  expp1zap  9674  expm1ap  9675  expubnd  9682  bernneq2  9743  expnlbnd  9746  omgadd  9878  hashun  9881  fihashssdif  9894  hashdifpr  9896  shftuz  9906  mulreap  9952  redivap  9962  imdivap  9969  resqrtcl  10116  climuni  10333  addcn2  10350  mulcn2  10352  dvdsval2  10406  addmodlteqALT  10467  modremain  10536  fldivndvdslt  10542  mulgcdr  10614  gcddiv  10615  rpmulgcd  10622  rplpwr  10623  rppwr  10624  qredeq  10685  divgcdcoprmex  10691  cncongr1  10692  cncongr2  10693  dvdsnprmd  10714  euclemma  10732  prmexpb  10737  qnumdenbi  10777  hashgcdlem  10810  unennn  10817  bdfind  11008
  Copyright terms: Public domain W3C validator