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

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

Proof of Theorem 3ad2ant3
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantl 266 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 933 1  |-  ( ( ps  /\  th  /\  ph )  ->  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:  simp3l  943  simp3r  944  simp31  951  simp32  952  simp33  953  simp3ll  986  simp3lr  987  simp3rl  988  simp3rr  989  simp3l1  1020  simp3l2  1021  simp3l3  1022  simp3r1  1023  simp3r2  1024  simp3r3  1025  simp31l  1038  simp31r  1039  simp32l  1040  simp32r  1041  simp33l  1042  simp33r  1043  simp311  1062  simp312  1063  simp313  1064  simp321  1065  simp322  1066  simp323  1067  simp331  1068  simp332  1069  simp333  1070  3anim123i  1100  3jaao  1214  ceqsalt  2597  ceqsralt  2598  vtoclgft  2621  ifbothdc  3385  tpssi  3558  sotricim  4088  elirr  4294  en2lp  4306  reg3exmidlemwe  4331  sotri2  4750  poltletr  4753  funprg  4977  funtpg  4978  fntpg  4983  funimaexglem  5010  fvun1  5267  ftpg  5375  fsnunf  5390  fsnunfv  5391  caovimo  5722  brtposg  5900  smoel  5946  rdgivallem  5999  frecsuclem1  6018  frecsuclemdm  6019  frecsuclem2  6020  frecsuclem3  6021  ltsopi  6476  distrnqg  6543  ltmnqg  6557  mulcanenq0ec  6601  distrnq0  6615  prarloclem5  6656  1idprl  6746  1idpru  6747  ltaprg  6775  recexprlemopl  6781  recexprlemopu  6783  recexprlem1ssl  6789  aptipr  6797  ltmprr  6798  cauappcvgprlemlol  6803  cauappcvgprlemupu  6805  caucvgprlemlol  6826  caucvgprlemupu  6828  caucvgprprlemlol  6854  caucvgprprlemupu  6856  readdcan  7214  cnegexlem2  7250  addcan2  7255  ltadd2  7488  apreap  7652  ltmul1  7657  apcotr  7672  apadd1  7673  mulext1  7677  divdirap  7748  divcanap5  7765  ltdiv1  7909  lt2halves  8217  zdivmul  8388  eluzsub  8598  ledivge1le  8750  addlelt  8786  elioo5  8903  iccsupr  8936  iccneg  8958  icoshft  8959  icoshftf1o  8960  zltaddlt1le  8975  fzen  9009  elfz1b  9054  fzrevral  9069  fzshftral  9072  elfz0ubfz0  9084  elfz0fzfz0  9085  fz0fzelfz0  9086  fz0fzdiffz0  9089  elfzo  9108  elfzonlteqm1  9168  modqaddmulmod  9341  expdivap  9471  leexp2a  9473  bcval3  9619  shftfibg  9649  elicc4abs  9921  mulcn2  10064  dvdsval2  10111  dvdsmulcr  10137  modmulconst  10139  dvdsexp  10173  oddge22np1  10193  modremain  10241  findset  10457
  Copyright terms: Public domain W3C validator