New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3impa | GIF version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impa.1 | ⊢ (((φ ∧ ψ) ∧ χ) → θ) |
Ref | Expression |
---|---|
3impa | ⊢ ((φ ∧ ψ ∧ χ) → θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impa.1 | . . 3 ⊢ (((φ ∧ ψ) ∧ χ) → θ) | |
2 | 1 | exp31 587 | . 2 ⊢ (φ → (ψ → (χ → θ))) |
3 | 2 | 3imp 1145 | 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: 3impdir 1238 syl3an9b 1250 biimp3a 1281 rspec3 2714 rspc3v 2964 raltpg 3777 rextpg 3778 eladdci 4399 lefinlteq 4463 opelopabt 4699 3optocl 4840 fun2ssres 5145 funssfv 5343 foco2 5426 f1elima 5474 eloprabga 5578 mucass 6135 cenc 6181 |
Copyright terms: Public domain | W3C validator |