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

Theorem 3ad2ant3 913
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 908 1 ((ψ θ φ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 871
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 873
This theorem is referenced by:  simp3l  918  simp3r  919  simp31  926  simp32  927  simp33  928  simp3ll  961  simp3lr  962  simp3rl  963  simp3rr  964  simp3l1  995  simp3l2  996  simp3l3  997  simp3r1  998  simp3r2  999  simp3r3  1000  simp31l  1013  simp31r  1014  simp32l  1015  simp32r  1016  simp33l  1017  simp33r  1018  simp311  1037  simp312  1038  simp313  1039  simp321  1040  simp322  1041  simp323  1042  simp331  1043  simp332  1044  simp333  1045  3anim123i  1074  3jaao  1186  ceqsalt  2553  ceqsralt  2554  vtoclgft  2577  tpssi  3500  sotricim  4030  elirr  4204  en2lp  4212  sotri2  4645  poltletr  4648  funprg  4871  funtpg  4872  fntpg  4877  funimaexglem  4904  fvun1  5160  ftpg  5268  fsnunf  5283  fsnunfv  5284  caovimo  5613  brtposg  5787  smoel  5833  rdgivallem  5884  frecsuclem1  5899  frecsuclemdm  5900  frecsuclem2  5901  frecsuclem3  5902  ltsopi  6174  distrnqg  6240  ltmnqg  6254  mulcanenq0ec  6294  distrnq0  6308  prarloclem5  6348  1idprl  6423  1idpru  6424  ltaprg  6449  recexprlemopl  6453  recexprlemopu  6455  recexprlem1ssl  6461  readdcan  6740  cnegexlem2  6774  addcan2  6779  ltadd2  7002  findset  7306
  Copyright terms: Public domain W3C validator