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

Theorem 3ad2ant2 1003
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 274 . 2  |-  ( (
ph  /\  th )  ->  ch )
323adant1 999 1  |-  ( ( ps  /\  ph  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  simp2l  1007  simp2r  1008  simp21  1014  simp22  1015  simp23  1016  simp2ll  1048  simp2lr  1049  simp2rl  1050  simp2rr  1051  simp2l1  1080  simp2l2  1081  simp2l3  1082  simp2r1  1083  simp2r2  1084  simp2r3  1085  simp21l  1098  simp21r  1099  simp22l  1100  simp22r  1101  simp23l  1102  simp23r  1103  simp211  1119  simp212  1120  simp213  1121  simp221  1122  simp222  1123  simp223  1124  simp231  1125  simp232  1126  simp233  1127  3anim123i  1166  3jaao  1286  ceqsalt  2712  vtoclgft  2736  vtoclegft  2758  ifbothdc  3504  frirrg  4272  elirr  4456  en2lp  4469  reg3exmidlemwe  4493  sotri3  4937  funtpg  5174  fnprg  5178  fntpg  5179  funimaexglem  5206  fnco  5231  fvun1  5487  oprssov  5912  caovimo  5964  rdgivallem  6278  fnsnsplitdc  6401  funresdfunsndc  6402  f1dom2g  6650  mapxpen  6742  ssfidc  6823  sbthlemi4  6848  ordiso2  6920  updjud  6967  difinfsn  6985  mkvprop  7032  endjudisj  7066  distrnqg  7195  distrnq0  7267  prarloclem5  7308  cauappcvgprlemlol  7455  cauappcvgprlemupu  7457  caucvgprlemlol  7478  caucvgprlemupu  7480  caucvgprprlemlol  7506  caucvgprprlemupu  7508  cnegexlem2  7938  apcotr  8369  apadd1  8370  mulext1  8374  div2negap  8495  ltdiv2  8645  nndivtr  8762  zdivmul  9141  gtndiv  9146  fzind  9166  eluzuzle  9334  eluzp1p1  9351  peano2uz  9378  qdivcl  9435  irrmul  9439  ledivge1le  9513  xrre2  9604  xaddass  9652  xltadd1  9659  xlt2add  9663  ubioc1  9712  ubicc2  9768  zltaddlt1le  9789  uzsubsubfz  9827  elfz1b  9870  fzp1nel  9884  fz0fzdiffz0  9907  difelfzle  9911  elfzo0  9959  elfzonlteqm1  9987  fzonn0p1p1  9990  fzosplitprm1  10011  fzoshftral  10015  subfzo0  10019  ceiqle  10086  modqval  10097  modqvalr  10098  flqpmodeq  10100  modq0  10102  mulqmod0  10103  negqmod0  10104  modqge0  10105  modqlt  10106  modqelico  10107  modqdiffl  10108  modqmulnn  10115  modqvalp1  10116  modqmuladdnn0  10141  qnegmod  10142  addmodid  10145  q2submod  10158  modifeq2int  10159  modfzo0difsn  10168  addmodlteq  10171  omgadd  10548  hashun  10551  redivap  10646  imdivap  10653  xrmaxltsup  11027  xrmaxadd  11030  xrlemininf  11040  xrminltinf  11041  climuni  11062  mulcn2  11081  fsumsplitsnun  11188  prodfap0  11314  efsub  11387  cos12dec  11474  summodnegmod  11524  divalglemex  11619  divalg  11621  modremain  11626  ndvdssub  11627  fldivndvdslt  11632  nndvdslegcd  11654  dfgcd2  11702  mulgcd  11704  mulgcdr  11706  gcddiv  11707  rplpwr  11715  rppwr  11716  qredeq  11777  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  pw2dvdslemn  11843  hashgcdlem  11903  unennn  11910  ntrin  12293  elnei  12321  restco  12343  cnpnei  12388  cncnp2m  12400  sslm  12416  upxp  12441  blres  12603  metcnp3  12680  tgqioo  12716  ptolemy  12905
  Copyright terms: Public domain W3C validator