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

Theorem 3ad2ant3 989
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 275 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 984 1  |-  ( ( ps  /\  th  /\  ph )  ->  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:  simp3l  994  simp3r  995  simp31  1002  simp32  1003  simp33  1004  simp3ll  1037  simp3lr  1038  simp3rl  1039  simp3rr  1040  simp3l1  1071  simp3l2  1072  simp3l3  1073  simp3r1  1074  simp3r2  1075  simp3r3  1076  simp31l  1089  simp31r  1090  simp32l  1091  simp32r  1092  simp33l  1093  simp33r  1094  simp311  1113  simp312  1114  simp313  1115  simp321  1116  simp322  1117  simp323  1118  simp331  1119  simp332  1120  simp333  1121  3anim123i  1151  3jaao  1271  ceqsalt  2686  ceqsralt  2687  vtoclgft  2710  ifbothdc  3474  tpssi  3656  sotricim  4215  elirr  4426  en2lp  4439  reg3exmidlemwe  4463  sotri2  4906  poltletr  4909  funprg  5143  funtpg  5144  fntpg  5149  funimaexglem  5176  fvun1  5455  ftpg  5572  fsnunf  5588  fsnunfv  5589  caovimo  5932  brtposg  6119  smoel  6165  rdgivallem  6246  frecsuclem  6271  mapxpen  6710  unsnfi  6775  unsnfidcex  6776  unsnfidcel  6777  sbthlemi4  6816  elfir  6829  updjud  6935  ltsopi  7096  distrnqg  7163  ltmnqg  7177  mulcanenq0ec  7221  distrnq0  7235  prarloclem5  7276  1idprl  7366  1idpru  7367  ltaprg  7395  recexprlemopl  7401  recexprlemopu  7403  recexprlem1ssl  7409  aptipr  7417  ltmprr  7418  cauappcvgprlemlol  7423  cauappcvgprlemupu  7425  caucvgprlemlol  7446  caucvgprlemupu  7448  caucvgprprlemlol  7474  caucvgprprlemupu  7476  readdcan  7870  cnegexlem2  7906  addcan2  7911  ltadd2  8149  apreap  8317  ltmul1  8322  apcotr  8337  apadd1  8338  mulext1  8342  divdirap  8425  divcanap5  8442  ltdiv1  8594  lt2halves  8923  zdivmul  9109  eluzsub  9323  ledivge1le  9481  addlelt  9523  xaddass  9620  xleadd1  9626  xltadd1  9627  elioo5  9684  iccsupr  9717  iccneg  9740  icoshft  9741  icoshftf1o  9742  zltaddlt1le  9757  fzen  9791  elfz1b  9838  fzrevral  9853  fzshftral  9856  elfz0ubfz0  9870  elfz0fzfz0  9871  fz0fzelfz0  9872  fz0fzdiffz0  9875  elfzo  9894  fzodcel  9897  elfzonlteqm1  9955  modqaddmulmod  10132  expdivap  10312  leexp2a  10314  bcval3  10465  omgadd  10516  shftfibg  10560  elicc4abs  10834  xrmaxltsup  10995  xrmaxadd  10998  xrlemininf  11008  xrminltinf  11009  mulcn2  11049  fsumsplitsnun  11156  demoivreALT  11407  dvdsval2  11423  dvdsmulcr  11450  modmulconst  11452  dvdsexp  11486  oddge22np1  11505  modremain  11553  mulgcd  11631  mulgcdr  11633  gcddiv  11634  rpmulgcd  11641  rplpwr  11642  coprmdvds  11700  cncongr1  11711  dvdsnprmd  11733  prmexpb  11756  rpexp  11758  cncongrprm  11762  isstructr  11901  setsvala  11917  setsresg  11924  strle3g  11978  clsss  12214  ntrcls0  12227  neiss  12246  neipsm  12250  cnpnei  12315  cncnp2m  12327  cnconst2  12329  sslm  12343  upxp  12368  txmetcn  12615  ptolemy  12832  sincosq1eq  12847  findset  13070
  Copyright terms: Public domain W3C validator