New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simp3l | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp3l | ⊢ ((φ ∧ ψ ∧ (χ ∧ θ)) → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 443 | . 2 ⊢ ((χ ∧ θ) → χ) | |
2 | 1 | 3ad2ant3 978 | 1 ⊢ ((φ ∧ ψ ∧ (χ ∧ θ)) → χ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 ∧ w3a 934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 df-3an 936 |
This theorem is referenced by: simpl3l 1010 simpr3l 1016 simp13l 1070 simp23l 1076 simp33l 1082 nnpw1ex 4484 tfinpw1 4494 tfinltfinlem1 4500 nnadjoin 4520 nnpweq 4523 sfin112 4529 sfindbl 4530 sfintfin 4532 sfinltfin 4535 funprgOLD 5150 fvopab4t 5385 |
Copyright terms: Public domain | W3C validator |