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

Theorem 3ad2ant3 927
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 262 . 2 ((𝜃𝜑) → 𝜒)
323adant1 922 1 ((𝜓𝜃𝜑) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  simp3l  932  simp3r  933  simp31  940  simp32  941  simp33  942  simp3ll  975  simp3lr  976  simp3rl  977  simp3rr  978  simp3l1  1009  simp3l2  1010  simp3l3  1011  simp3r1  1012  simp3r2  1013  simp3r3  1014  simp31l  1027  simp31r  1028  simp32l  1029  simp32r  1030  simp33l  1031  simp33r  1032  simp311  1051  simp312  1052  simp313  1053  simp321  1054  simp322  1055  simp323  1056  simp331  1057  simp332  1058  simp333  1059  3anim123i  1089  3jaao  1203  ceqsalt  2580  ceqsralt  2581  vtoclgft  2604  ifbothdc  3357  tpssi  3530  sotricim  4060  elirr  4266  en2lp  4278  reg3exmidlemwe  4303  sotri2  4722  poltletr  4725  funprg  4949  funtpg  4950  fntpg  4955  funimaexglem  4982  fvun1  5239  ftpg  5347  fsnunf  5362  fsnunfv  5363  caovimo  5694  brtposg  5869  smoel  5915  rdgivallem  5968  frecsuclem1  5987  frecsuclemdm  5988  frecsuclem2  5989  frecsuclem3  5990  ltsopi  6416  distrnqg  6483  ltmnqg  6497  mulcanenq0ec  6541  distrnq0  6555  prarloclem5  6596  1idprl  6686  1idpru  6687  ltaprg  6715  recexprlemopl  6721  recexprlemopu  6723  recexprlem1ssl  6729  aptipr  6737  ltmprr  6738  cauappcvgprlemlol  6743  cauappcvgprlemupu  6745  caucvgprlemlol  6766  caucvgprlemupu  6768  caucvgprprlemlol  6794  caucvgprprlemupu  6796  readdcan  7151  cnegexlem2  7185  addcan2  7190  ltadd2  7414  apreap  7576  ltmul1  7581  apcotr  7596  apadd1  7597  mulext1  7601  divdirap  7672  divcanap5  7688  ltdiv1  7832  lt2halves  8158  zdivmul  8328  eluzsub  8500  ledivge1le  8650  elioo5  8800  iccsupr  8833  iccneg  8855  icoshft  8856  icoshftf1o  8857  fzen  8905  elfz1b  8950  fzrevral  8965  fzshftral  8968  elfz0ubfz0  8980  elfz0fzfz0  8981  fz0fzelfz0  8982  fz0fzdiffz0  8985  elfzo  9004  elfzonlteqm1  9064  expdivap  9303  leexp2a  9305  shftfibg  9419  elicc4abs  9688  mulcn2  9831  findset  10068
  Copyright terms: Public domain W3C validator