NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  3ad2ant3 GIF version

Theorem 3ad2ant3 978
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 452 . 2 ((θ φ) → χ)
323adant1 973 1 ((ψ θ φ) → χ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   w3a 934
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
This theorem is referenced by:  simp3l  983  simp3r  984  simp31  991  simp32  992  simp33  993  simp3ll  1026  simp3lr  1027  simp3rl  1028  simp3rr  1029  simp3l1  1060  simp3l2  1061  simp3l3  1062  simp3r1  1063  simp3r2  1064  simp3r3  1065  simp31l  1078  simp31r  1079  simp32l  1080  simp32r  1081  simp33l  1082  simp33r  1083  simp311  1102  simp312  1103  simp313  1104  simp321  1105  simp322  1106  simp323  1107  simp331  1108  simp332  1109  simp333  1110  3anim123i  1137  3jaao  1249  ceqsalt  2881  ceqsralt  2882  vtoclgft  2905  nnsucelrlem3  4426  nnsucelr  4428  ltfintri  4466  ssfin  4470  tfin11  4493  tfinltfinlem1  4500  sfintfin  4532  sfin111  4536  funprg  5149  fnprg  5153  fvun1  5379  ider  5943  ssetpov  5944  eqer  5961  elmapg  6012  elpmg  6013  ener  6039  enadj  6060  enprmaplem6  6081  nenpw1pwlem2  6085  elce  6175  addlec  6208  lenc  6223  taddc  6229
  Copyright terms: Public domain W3C validator