Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3expib | GIF version |
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3expib | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3exp 1180 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 252 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: 3anidm12 1273 mob 2866 eqbrrdva 4709 funimaexglem 5206 fco 5288 f1oiso2 5728 caovimo 5964 smoel2 6200 nnaword 6407 3ecoptocl 6518 sbthlemi10 6854 distrnq0 7267 addassnq0 7270 prcdnql 7292 prcunqu 7293 genpdisj 7331 cauappcvgprlemrnd 7458 caucvgprlemrnd 7481 caucvgprprlemrnd 7509 nn0n0n1ge2b 9130 fzind 9166 icoshft 9773 fzen 9823 seq3coll 10585 shftuz 10589 mulgcd 11704 algcvga 11732 lcmneg 11755 blssps 12596 blss 12597 metcnp3 12680 sincosq1sgn 12907 sincosq2sgn 12908 sincosq3sgn 12909 sincosq4sgn 12910 |
Copyright terms: Public domain | W3C validator |