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

Theorem 3ad2ant2 988
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 984 1  |-  ( ( ps  /\  ph  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 947
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 949
This theorem is referenced by:  simp2l  992  simp2r  993  simp21  999  simp22  1000  simp23  1001  simp2ll  1033  simp2lr  1034  simp2rl  1035  simp2rr  1036  simp2l1  1065  simp2l2  1066  simp2l3  1067  simp2r1  1068  simp2r2  1069  simp2r3  1070  simp21l  1083  simp21r  1084  simp22l  1085  simp22r  1086  simp23l  1087  simp23r  1088  simp211  1104  simp212  1105  simp213  1106  simp221  1107  simp222  1108  simp223  1109  simp231  1110  simp232  1111  simp233  1112  3anim123i  1151  3jaao  1271  ceqsalt  2686  vtoclgft  2710  vtoclegft  2732  ifbothdc  3474  frirrg  4242  elirr  4426  en2lp  4439  reg3exmidlemwe  4463  sotri3  4907  funtpg  5144  fnprg  5148  fntpg  5149  funimaexglem  5176  fnco  5201  fvun1  5455  oprssov  5880  caovimo  5932  rdgivallem  6246  fnsnsplitdc  6369  funresdfunsndc  6370  f1dom2g  6618  mapxpen  6710  ssfidc  6791  sbthlemi4  6816  ordiso2  6888  updjud  6935  difinfsn  6953  mkvprop  7000  endjudisj  7034  distrnqg  7163  distrnq0  7235  prarloclem5  7276  cauappcvgprlemlol  7423  cauappcvgprlemupu  7425  caucvgprlemlol  7446  caucvgprlemupu  7448  caucvgprprlemlol  7474  caucvgprprlemupu  7476  cnegexlem2  7906  apcotr  8337  apadd1  8338  mulext1  8342  div2negap  8463  ltdiv2  8613  nndivtr  8730  zdivmul  9109  gtndiv  9114  fzind  9134  eluzuzle  9302  eluzp1p1  9319  peano2uz  9346  qdivcl  9403  irrmul  9407  ledivge1le  9481  xrre2  9572  xaddass  9620  xltadd1  9627  xlt2add  9631  ubioc1  9680  ubicc2  9736  zltaddlt1le  9757  uzsubsubfz  9795  elfz1b  9838  fzp1nel  9852  fz0fzdiffz0  9875  difelfzle  9879  elfzo0  9927  elfzonlteqm1  9955  fzonn0p1p1  9958  fzosplitprm1  9979  fzoshftral  9983  subfzo0  9987  ceiqle  10054  modqval  10065  modqvalr  10066  flqpmodeq  10068  modq0  10070  mulqmod0  10071  negqmod0  10072  modqge0  10073  modqlt  10074  modqelico  10075  modqdiffl  10076  modqmulnn  10083  modqvalp1  10084  modqmuladdnn0  10109  qnegmod  10110  addmodid  10113  q2submod  10126  modifeq2int  10127  modfzo0difsn  10136  addmodlteq  10139  omgadd  10516  hashun  10519  redivap  10614  imdivap  10621  xrmaxltsup  10995  xrmaxadd  10998  xrlemininf  11008  xrminltinf  11009  climuni  11030  mulcn2  11049  fsumsplitsnun  11156  efsub  11314  cos12dec  11401  summodnegmod  11451  divalglemex  11546  divalg  11548  modremain  11553  ndvdssub  11554  fldivndvdslt  11559  nndvdslegcd  11581  dfgcd2  11629  mulgcd  11631  mulgcdr  11633  gcddiv  11634  rplpwr  11642  rppwr  11643  qredeq  11704  divgcdcoprmex  11710  cncongr1  11711  cncongr2  11712  pw2dvdslemn  11770  hashgcdlem  11830  unennn  11837  ntrin  12220  elnei  12248  restco  12270  cnpnei  12315  cncnp2m  12327  sslm  12343  upxp  12368  blres  12530  metcnp3  12607  tgqioo  12643  ptolemy  12832
  Copyright terms: Public domain W3C validator