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

Theorem 3ad2ant1 924
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1
Assertion
Ref Expression
3ad2ant1

Proof of Theorem 3ad2ant1
StepHypRef Expression
1 3ad2ant.1 . . 3
21adantr 261 . 2
323adant2 922 1
Colors of variables: wff set class
Syntax hints:   wi 4   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  simp1l  927  simp1r  928  simp11  933  simp12  934  simp13  935  simp1ll  966  simp1lr  967  simp1rl  968  simp1rr  969  simp1l1  996  simp1l2  997  simp1l3  998  simp1r1  999  simp1r2  1000  simp1r3  1001  simp11l  1014  simp11r  1015  simp12l  1016  simp12r  1017  simp13l  1018  simp13r  1019  simp111  1032  simp112  1033  simp113  1034  simp121  1035  simp122  1036  simp123  1037  simp131  1038  simp132  1039  simp133  1040  3anim123i  1088  3jaao  1202  ceqsalt  2574  sbciegft  2787  reupick2  3217  breldmg  4484  fntpg  4898  funimaexglem  4925  fex2  5002  fvun1  5182  fprg  5289  fsnunfv  5306  fnfvima  5336  cocan1  5370  cocan2  5371  mpt2fvex  5771  poxp  5794  smoiso  5858  tfrlem5  5871  tfrlemibxssdm  5882  nnawordex  6037  mulcanenq0ec  6428  prltlu  6470  prarloclem3step  6479  prarloclem5  6483  ltasrg  6698  cnegexlem1  6983  addcan  6988  apcotr  7391  apadd1  7392  mulext1  7396  divdivap1  7481  divdivap2  7482  div2negap  7493  divneg2ap  7494  ltmulgt11  7611  ltdiv2  7634  squeeze0  7651  nndivtr  7736  nn0n0n1ge2  8087  zdivmul  8106  gtndiv  8111  eluzuzle  8257  eluzp1p1  8274  qdivcl  8352  irrmul  8356  rpgecl  8386  lbico1  8569  lbicc2  8622  uzsubsubfz  8681  elfz1b  8722  elfz0ubfz0  8752  fz0fzelfz0  8754  difelfzle  8762  difelfznle  8763  2ffzeq  8768  fzo1fzo0n0  8809  ubmelfzo  8826  fzonn0p1p1  8839  elfzom1p1elfzo  8840  elfzonelfzo  8856  qexpclz  8930  expgt1  8947  expp1zap  8957  expm1ap  8958  expubnd  8965  bernneq2  9023  expnlbnd  9026  mulreap  9092  redivap  9102  imdivap  9109  bdfind  9406
  Copyright terms: Public domain W3C validator