ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3ad2ant3 Structured version   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  6427  distrnq0  6441  prarloclem5  6482  1idprl  6565  1idpru  6566  ltaprg  6591  recexprlemopl  6596  recexprlemopu  6598  recexprlem1ssl  6604  aptipr  6612  ltmprr  6613  cauappcvgprlemlol  6618  cauappcvgprlemupu  6620  readdcan  6930  cnegexlem2  6964  addcan2  6969  ltadd2  7192  apreap  7351  ltmul1  7356  apcotr  7371  apadd1  7372  mulext1  7376  divdirap  7436  divcanap5  7452  ltdiv1  7595  lt2halves  7917  zdivmul  8086  eluzsub  8258  elioo5  8552  iccsupr  8585  iccneg  8607  icoshft  8608  icoshftf1o  8609  fzen  8657  elfz1b  8702  fzrevral  8717  fzshftral  8720  elfz0ubfz0  8732  elfz0fzfz0  8733  fz0fzelfz0  8734  fz0fzdiffz0  8737  elfzo  8756  elfzonlteqm1  8816  expdivap  8939  leexp2a  8941  findset  9379
  Copyright terms: Public domain W3C validator