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

Theorem 3ad2ant3 966
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 271 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 961 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  simp3l  971  simp3r  972  simp31  979  simp32  980  simp33  981  simp3ll  1014  simp3lr  1015  simp3rl  1016  simp3rr  1017  simp3l1  1048  simp3l2  1049  simp3l3  1050  simp3r1  1051  simp3r2  1052  simp3r3  1053  simp31l  1066  simp31r  1067  simp32l  1068  simp32r  1069  simp33l  1070  simp33r  1071  simp311  1090  simp312  1091  simp313  1092  simp321  1093  simp322  1094  simp323  1095  simp331  1096  simp332  1097  simp333  1098  3anim123i  1128  3jaao  1244  ceqsalt  2645  ceqsralt  2646  vtoclgft  2669  ifbothdc  3419  tpssi  3598  sotricim  4141  elirr  4347  en2lp  4360  reg3exmidlemwe  4384  sotri2  4816  poltletr  4819  funprg  5050  funtpg  5051  fntpg  5056  funimaexglem  5083  fvun1  5354  ftpg  5465  fsnunf  5480  fsnunfv  5481  caovimo  5820  brtposg  6001  smoel  6047  rdgivallem  6128  frecsuclem  6153  mapxpen  6544  unsnfi  6609  unsnfidcex  6610  unsnfidcel  6611  sbthlemi4  6648  updjud  6752  ltsopi  6858  distrnqg  6925  ltmnqg  6939  mulcanenq0ec  6983  distrnq0  6997  prarloclem5  7038  1idprl  7128  1idpru  7129  ltaprg  7157  recexprlemopl  7163  recexprlemopu  7165  recexprlem1ssl  7171  aptipr  7179  ltmprr  7180  cauappcvgprlemlol  7185  cauappcvgprlemupu  7187  caucvgprlemlol  7208  caucvgprlemupu  7210  caucvgprprlemlol  7236  caucvgprprlemupu  7238  readdcan  7601  cnegexlem2  7637  addcan2  7642  ltadd2  7876  apreap  8040  ltmul1  8045  apcotr  8060  apadd1  8061  mulext1  8065  divdirap  8138  divcanap5  8155  ltdiv1  8301  lt2halves  8621  zdivmul  8806  eluzsub  9017  ledivge1le  9172  addlelt  9208  elioo5  9320  iccsupr  9353  iccneg  9375  icoshft  9376  icoshftf1o  9377  zltaddlt1le  9392  fzen  9426  elfz1b  9471  fzrevral  9486  fzshftral  9489  elfz0ubfz0  9501  elfz0fzfz0  9502  fz0fzelfz0  9503  fz0fzdiffz0  9506  elfzo  9525  fzodcel  9528  elfzonlteqm1  9586  modqaddmulmod  9763  expdivap  9970  leexp2a  9972  bcval3  10123  omgadd  10174  shftfibg  10218  elicc4abs  10491  mulcn2  10664  fsumsplitsnun  10774  dvdsval2  10879  dvdsmulcr  10906  modmulconst  10908  dvdsexp  10942  oddge22np1  10961  modremain  11009  mulgcd  11085  mulgcdr  11087  gcddiv  11088  rpmulgcd  11095  rplpwr  11096  coprmdvds  11154  cncongr1  11165  dvdsnprmd  11187  prmexpb  11210  rpexp  11212  cncongrprm  11216  findset  11484
  Copyright terms: Public domain W3C validator