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

Theorem 3ad2ant3 962
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 271 . 2 ((𝜃𝜑) → 𝜒)
323adant1 957 1 ((𝜓𝜃𝜑) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
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 922
This theorem is referenced by:  simp3l  967  simp3r  968  simp31  975  simp32  976  simp33  977  simp3ll  1010  simp3lr  1011  simp3rl  1012  simp3rr  1013  simp3l1  1044  simp3l2  1045  simp3l3  1046  simp3r1  1047  simp3r2  1048  simp3r3  1049  simp31l  1062  simp31r  1063  simp32l  1064  simp32r  1065  simp33l  1066  simp33r  1067  simp311  1086  simp312  1087  simp313  1088  simp321  1089  simp322  1090  simp323  1091  simp331  1092  simp332  1093  simp333  1094  3anim123i  1124  3jaao  1240  ceqsalt  2626  ceqsralt  2627  vtoclgft  2650  ifbothdc  3388  tpssi  3559  sotricim  4086  elirr  4292  en2lp  4305  reg3exmidlemwe  4329  sotri2  4752  poltletr  4755  funprg  4980  funtpg  4981  fntpg  4986  funimaexglem  5013  fvun1  5271  ftpg  5379  fsnunf  5394  fsnunfv  5395  caovimo  5725  brtposg  5903  smoel  5949  rdgivallem  6030  frecsuclem  6055  unsnfi  6439  unsnfidcex  6440  unsnfidcel  6441  ltsopi  6572  distrnqg  6639  ltmnqg  6653  mulcanenq0ec  6697  distrnq0  6711  prarloclem5  6752  1idprl  6842  1idpru  6843  ltaprg  6871  recexprlemopl  6877  recexprlemopu  6879  recexprlem1ssl  6885  aptipr  6893  ltmprr  6894  cauappcvgprlemlol  6899  cauappcvgprlemupu  6901  caucvgprlemlol  6922  caucvgprlemupu  6924  caucvgprprlemlol  6950  caucvgprprlemupu  6952  readdcan  7315  cnegexlem2  7351  addcan2  7356  ltadd2  7590  apreap  7754  ltmul1  7759  apcotr  7774  apadd1  7775  mulext1  7779  divdirap  7852  divcanap5  7869  ltdiv1  8013  lt2halves  8333  zdivmul  8518  eluzsub  8729  ledivge1le  8884  addlelt  8920  elioo5  9032  iccsupr  9065  iccneg  9087  icoshft  9088  icoshftf1o  9089  zltaddlt1le  9104  fzen  9138  elfz1b  9183  fzrevral  9198  fzshftral  9201  elfz0ubfz0  9213  elfz0fzfz0  9214  fz0fzelfz0  9215  fz0fzdiffz0  9218  elfzo  9236  elfzonlteqm1  9296  modqaddmulmod  9473  expdivap  9624  leexp2a  9626  bcval3  9775  omgadd  9826  shftfibg  9846  elicc4abs  10118  mulcn2  10289  dvdsval2  10343  dvdsmulcr  10370  modmulconst  10372  dvdsexp  10406  oddge22np1  10425  modremain  10473  mulgcd  10549  mulgcdr  10551  gcddiv  10552  rpmulgcd  10559  rplpwr  10560  coprmdvds  10618  cncongr1  10629  dvdsnprmd  10651  prmexpb  10674  rpexp  10676  cncongrprm  10680  findset  10898
  Copyright terms: Public domain W3C validator