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

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

Proof of Theorem 3ad2ant2
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantr 265 . 2  |-  ( (
ph  /\  th )  ->  ch )
323adant1 933 1  |-  ( ( ps  /\  ph  /\  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:  simp2l  941  simp2r  942  simp21  948  simp22  949  simp23  950  simp2ll  982  simp2lr  983  simp2rl  984  simp2rr  985  simp2l1  1014  simp2l2  1015  simp2l3  1016  simp2r1  1017  simp2r2  1018  simp2r3  1019  simp21l  1032  simp21r  1033  simp22l  1034  simp22r  1035  simp23l  1036  simp23r  1037  simp211  1053  simp212  1054  simp213  1055  simp221  1056  simp222  1057  simp223  1058  simp231  1059  simp232  1060  simp233  1061  3anim123i  1100  3jaao  1214  ceqsalt  2597  vtoclgft  2621  vtoclegft  2642  ifbothdc  3385  frirrg  4115  elirr  4294  en2lp  4306  reg3exmidlemwe  4331  sotri3  4751  funtpg  4978  fnprg  4982  fntpg  4983  funimaexglem  5010  fnco  5035  fvun1  5267  oprssov  5670  caovimo  5722  rdgivallem  5999  f1dom2g  6267  ordiso2  6415  distrnqg  6543  distrnq0  6615  prarloclem5  6656  cauappcvgprlemlol  6803  cauappcvgprlemupu  6805  caucvgprlemlol  6826  caucvgprlemupu  6828  caucvgprprlemlol  6854  caucvgprprlemupu  6856  cnegexlem2  7250  apcotr  7672  apadd1  7673  mulext1  7677  div2negap  7786  ltdiv2  7928  nndivtr  8031  zdivmul  8388  gtndiv  8393  fzind  8412  eluzuzle  8577  eluzp1p1  8594  peano2uz  8622  qdivcl  8675  irrmul  8679  ledivge1le  8750  xrre2  8835  ubioc1  8899  ubicc2  8954  zltaddlt1le  8975  uzsubsubfz  9013  elfz1b  9054  fzp1nel  9068  fz0fzdiffz0  9089  difelfzle  9094  elfzo0  9140  elfzonlteqm1  9168  fzonn0p1p1  9171  fzosplitprm1  9192  fzoshftral  9196  subfzo0  9199  ceiqle  9263  modqval  9274  modqvalr  9275  flqpmodeq  9277  modq0  9279  mulqmod0  9280  negqmod0  9281  modqge0  9282  modqlt  9283  modqelico  9284  modqdiffl  9285  modqmulnn  9292  modqvalp1  9293  modqmuladdnn0  9318  qnegmod  9319  addmodid  9322  q2submod  9335  modifeq2int  9336  modfzo0difsn  9345  addmodlteq  9348  expival  9422  redivap  9702  imdivap  9709  climuni  10045  mulcn2  10064  summodnegmod  10138  divalglemex  10234  divalg  10236  modremain  10241  ndvdssub  10242  fldivndvdslt  10247  pw2dvdslemn  10253
  Copyright terms: Public domain W3C validator