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

Theorem 3ad2ant3 1005
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1 (𝜑𝜒)
Assertion
Ref Expression
3ad2ant3 ((𝜓𝜃𝜑) → 𝜒)

Proof of Theorem 3ad2ant3
StepHypRef Expression
1 3ad2ant.1 . . 3 (𝜑𝜒)
21adantl 275 . 2 ((𝜃𝜑) → 𝜒)
323adant1 1000 1 ((𝜓𝜃𝜑) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 963
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 965
This theorem is referenced by:  simp3l  1010  simp3r  1011  simp31  1018  simp32  1019  simp33  1020  simp3ll  1053  simp3lr  1054  simp3rl  1055  simp3rr  1056  simp3l1  1087  simp3l2  1088  simp3l3  1089  simp3r1  1090  simp3r2  1091  simp3r3  1092  simp31l  1105  simp31r  1106  simp32l  1107  simp32r  1108  simp33l  1109  simp33r  1110  simp311  1129  simp312  1130  simp313  1131  simp321  1132  simp322  1133  simp323  1134  simp331  1135  simp332  1136  simp333  1137  3anim123i  1167  3jaao  1287  ceqsalt  2715  ceqsralt  2716  vtoclgft  2739  ifbothdc  3508  tpssi  3693  sotricim  4252  elirr  4463  en2lp  4476  reg3exmidlemwe  4500  sotri2  4943  poltletr  4946  funprg  5180  funtpg  5181  fntpg  5186  funimaexglem  5213  fvun1  5494  ftpg  5611  fsnunf  5627  fsnunfv  5628  caovimo  5971  brtposg  6158  smoel  6204  rdgivallem  6285  frecsuclem  6310  mapxpen  6749  unsnfi  6814  unsnfidcex  6815  unsnfidcel  6816  sbthlemi4  6855  elfir  6868  updjud  6974  ltsopi  7151  distrnqg  7218  ltmnqg  7232  mulcanenq0ec  7276  distrnq0  7290  prarloclem5  7331  1idprl  7421  1idpru  7422  ltaprg  7450  recexprlemopl  7456  recexprlemopu  7458  recexprlem1ssl  7464  aptipr  7472  ltmprr  7473  cauappcvgprlemlol  7478  cauappcvgprlemupu  7480  caucvgprlemlol  7501  caucvgprlemupu  7503  caucvgprprlemlol  7529  caucvgprprlemupu  7531  readdcan  7925  cnegexlem2  7961  addcan2  7966  ltadd2  8204  apreap  8372  ltmul1  8377  apcotr  8392  apadd1  8393  mulext1  8397  divdirap  8480  divcanap5  8497  ltdiv1  8649  lt2halves  8978  zdivmul  9164  eluzsub  9378  ledivge1le  9542  addlelt  9584  xaddass  9681  xleadd1  9687  xltadd1  9688  elioo5  9745  iccsupr  9778  iccneg  9801  icoshft  9802  icoshftf1o  9803  zltaddlt1le  9819  fzen  9853  elfz1b  9900  fzrevral  9915  fzshftral  9918  elfz0ubfz0  9932  elfz0fzfz0  9933  fz0fzelfz0  9934  fz0fzdiffz0  9937  elfzo  9956  fzodcel  9959  elfzonlteqm1  10017  modqaddmulmod  10194  expdivap  10374  leexp2a  10376  bcval3  10528  omgadd  10579  shftfibg  10623  elicc4abs  10897  xrmaxltsup  11058  xrmaxadd  11061  xrlemininf  11071  xrminltinf  11072  mulcn2  11112  fsumsplitsnun  11219  prodfrecap  11346  demoivreALT  11514  dvdsval2  11530  dvdsmulcr  11557  modmulconst  11559  dvdsexp  11593  oddge22np1  11612  modremain  11660  mulgcd  11738  mulgcdr  11740  gcddiv  11741  rpmulgcd  11748  rplpwr  11749  coprmdvds  11807  cncongr1  11818  dvdsnprmd  11840  prmexpb  11863  rpexp  11865  cncongrprm  11869  isstructr  12011  setsvala  12027  setsresg  12034  strle3g  12088  clsss  12324  ntrcls0  12337  neiss  12356  neipsm  12360  cnpnei  12425  cncnp2m  12437  cnconst2  12439  sslm  12453  upxp  12478  txmetcn  12725  ptolemy  12951  sincosq1eq  12966  rplogbval  13068  rpcxplogb  13087  findset  13312
  Copyright terms: Public domain W3C validator