Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3exp1 | Structured version Visualization version GIF version |
Description: Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
3exp1.1 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
3exp1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp1.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
2 | 1 | ex 413 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏)) |
3 | 2 | 3exp 1111 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: 3an1rs 1351 funelss 7735 ltmpi 10314 cshf1 14160 lcmfunsnlem 15973 mulgaddcom 18189 mulginvcom 18190 symgfvne 18444 voliunlem3 24080 3cyclfrgrrn 27992 numclwwlk1lem2foa 28060 frgrregord013 28101 strlem3a 29956 hstrlem3a 29964 chirredlem1 30094 nn0prpwlem 33567 matunitlindflem1 34769 zerdivemp1x 35106 athgt 36472 paddasslem14 36849 paddidm 36857 tendospcanN 38039 jm2.26 39477 relexpxpmin 39940 0ellimcdiv 41806 |
Copyright terms: Public domain | W3C validator |