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

Theorem 3ad2ant1 936
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 265 . 2  |-  ( (
ph  /\  th )  ->  ch )
323adant2 934 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simp1l  939  simp1r  940  simp11  945  simp12  946  simp13  947  simp1ll  978  simp1lr  979  simp1rl  980  simp1rr  981  simp1l1  1008  simp1l2  1009  simp1l3  1010  simp1r1  1011  simp1r2  1012  simp1r3  1013  simp11l  1026  simp11r  1027  simp12l  1028  simp12r  1029  simp13l  1030  simp13r  1031  simp111  1044  simp112  1045  simp113  1046  simp121  1047  simp122  1048  simp123  1049  simp131  1050  simp132  1051  simp133  1052  3anim123i  1100  3jaao  1214  ceqsalt  2597  sbciegft  2815  reupick2  3250  ifbothdc  3384  frirrg  4114  breldmg  4568  fntpg  4982  funimaexglem  5009  fex2  5086  fvun1  5266  fprg  5373  fsnunfv  5390  fnfvima  5420  cocan1  5454  cocan2  5455  mpt2fvex  5856  poxp  5880  smoiso  5947  tfrlem5  5960  tfrlemibxssdm  5971  nnawordex  6131  fidceq  6360  fidifsnen  6361  dif1en  6367  ordiso2  6414  mulcanenq0ec  6600  prltlu  6642  prarloclem3step  6651  prarloclem5  6655  ltasrg  6912  cnegexlem1  7248  addcan  7253  apcotr  7671  apadd1  7672  mulext1  7676  divdivap1  7773  divdivap2  7774  div2negap  7785  divneg2ap  7786  ltmulgt11  7904  ltdiv2  7927  squeeze0  7944  nndivtr  8030  nn0n0n1ge2  8368  zdivmul  8387  gtndiv  8392  eluzuzle  8576  eluzp1p1  8593  qdivcl  8674  irrmul  8678  rpgecl  8708  lbico1  8899  lbicc2  8952  zltaddlt1le  8974  uzsubsubfz  9012  elfz1b  9053  elfz0ubfz0  9083  fz0fzelfz0  9085  difelfzle  9093  difelfznle  9094  2ffzeq  9099  fzo1fzo0n0  9140  ubmelfzo  9157  fzonn0p1p1  9170  elfzom1p1elfzo  9171  elfzonelfzo  9187  subfzo0  9198  ceiqle  9257  ceilqle  9258  modqval  9268  flqpmodeq  9271  modq0  9273  negqmod0  9275  modqge0  9276  modqlt  9277  modqdiffl  9279  modqmulnn  9286  modqvalp1  9287  modqmuladdnn0  9312  qnegmod  9313  addmodid  9316  modfzo0difsn  9339  addmodlteq  9342  qexpclz  9435  expgt1  9452  expp1zap  9463  expm1ap  9464  expubnd  9471  bernneq2  9531  expnlbnd  9534  shftuz  9639  mulreap  9685  redivap  9695  imdivap  9702  resqrtcl  9848  climuni  10037  addcn2  10054  mulcn2  10056  dvdsval2  10103  addmodlteqALT  10163  bdfind  10430
  Copyright terms: Public domain W3C validator