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

Theorem 3ad2ant1 924
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1 (φχ)
Assertion
Ref Expression
3ad2ant1 ((φ ψ θ) → χ)

Proof of Theorem 3ad2ant1
StepHypRef Expression
1 3ad2ant.1 . . 3 (φχ)
21adantr 261 . 2 ((φ θ) → χ)
323adant2 922 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:  simp1l  927  simp1r  928  simp11  933  simp12  934  simp13  935  simp1ll  966  simp1lr  967  simp1rl  968  simp1rr  969  simp1l1  996  simp1l2  997  simp1l3  998  simp1r1  999  simp1r2  1000  simp1r3  1001  simp11l  1014  simp11r  1015  simp12l  1016  simp12r  1017  simp13l  1018  simp13r  1019  simp111  1032  simp112  1033  simp113  1034  simp121  1035  simp122  1036  simp123  1037  simp131  1038  simp132  1039  simp133  1040  3anim123i  1088  3jaao  1202  ceqsalt  2574  sbciegft  2787  reupick2  3217  breldmg  4484  fntpg  4898  funimaexglem  4925  fex2  5002  fvun1  5182  fprg  5289  fsnunfv  5306  fnfvima  5336  cocan1  5370  cocan2  5371  mpt2fvex  5771  poxp  5794  smoiso  5858  tfrlem5  5871  tfrlemibxssdm  5882  nnawordex  6037  mulcanenq0ec  6427  prltlu  6469  prarloclem3step  6478  prarloclem5  6482  ltasrg  6678  cnegexlem1  6963  addcan  6968  apcotr  7371  apadd1  7372  mulext1  7376  divdivap1  7461  divdivap2  7462  div2negap  7473  divneg2ap  7474  ltmulgt11  7591  ltdiv2  7614  squeeze0  7631  nndivtr  7716  nn0n0n1ge2  8067  zdivmul  8086  gtndiv  8091  eluzuzle  8237  eluzp1p1  8254  qdivcl  8332  irrmul  8336  rpgecl  8366  lbico1  8549  lbicc2  8602  uzsubsubfz  8661  elfz1b  8702  elfz0ubfz0  8732  fz0fzelfz0  8734  difelfzle  8742  difelfznle  8743  2ffzeq  8748  fzo1fzo0n0  8789  ubmelfzo  8806  fzonn0p1p1  8819  elfzom1p1elfzo  8820  elfzonelfzo  8836  qexpclz  8910  expgt1  8927  expp1zap  8937  expm1ap  8938  expubnd  8945  bernneq2  9003  expnlbnd  9006  mulreap  9072  redivap  9082  imdivap  9089  bdfind  9380
  Copyright terms: Public domain W3C validator