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

Theorem 3ad2ant3 926
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 921 1 ((ψ θ φ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 884
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 886
This theorem is referenced by:  simp3l  931  simp3r  932  simp31  939  simp32  940  simp33  941  simp3ll  974  simp3lr  975  simp3rl  976  simp3rr  977  simp3l1  1008  simp3l2  1009  simp3l3  1010  simp3r1  1011  simp3r2  1012  simp3r3  1013  simp31l  1026  simp31r  1027  simp32l  1028  simp32r  1029  simp33l  1030  simp33r  1031  simp311  1050  simp312  1051  simp313  1052  simp321  1053  simp322  1054  simp323  1055  simp331  1056  simp332  1057  simp333  1058  3anim123i  1088  3jaao  1202  ceqsalt  2574  ceqsralt  2575  vtoclgft  2598  tpssi  3521  sotricim  4051  elirr  4224  en2lp  4232  sotri2  4665  poltletr  4668  funprg  4892  funtpg  4893  fntpg  4898  funimaexglem  4925  fvun1  5182  ftpg  5290  fsnunf  5305  fsnunfv  5306  caovimo  5636  brtposg  5810  smoel  5856  rdgivallem  5908  frecsuclem1  5926  frecsuclemdm  5927  frecsuclem2  5928  frecsuclem3  5929  ltsopi  6304  distrnqg  6371  ltmnqg  6385  mulcanenq0ec  6428  distrnq0  6442  prarloclem5  6483  1idprl  6566  1idpru  6567  ltaprg  6592  recexprlemopl  6597  recexprlemopu  6599  recexprlem1ssl  6605  aptipr  6613  ltmprr  6614  cauappcvgprlemlol  6619  cauappcvgprlemupu  6621  caucvgprlemlol  6641  caucvgprlemupu  6643  readdcan  6950  cnegexlem2  6984  addcan2  6989  ltadd2  7212  apreap  7371  ltmul1  7376  apcotr  7391  apadd1  7392  mulext1  7396  divdirap  7456  divcanap5  7472  ltdiv1  7615  lt2halves  7937  zdivmul  8106  eluzsub  8278  elioo5  8572  iccsupr  8605  iccneg  8627  icoshft  8628  icoshftf1o  8629  fzen  8677  elfz1b  8722  fzrevral  8737  fzshftral  8740  elfz0ubfz0  8752  elfz0fzfz0  8753  fz0fzelfz0  8754  fz0fzdiffz0  8757  elfzo  8776  elfzonlteqm1  8836  expdivap  8959  leexp2a  8961  findset  9405
  Copyright terms: Public domain W3C validator