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 1184 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 252 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 963 |
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 965 |
This theorem is referenced by: 3anidm12 1277 mob 2894 eqbrrdva 4756 funimaexglem 5253 fco 5335 f1oiso2 5777 caovimo 6014 smoel2 6250 nnaword 6458 3ecoptocl 6569 sbthlemi10 6910 distrnq0 7379 addassnq0 7382 prcdnql 7404 prcunqu 7405 genpdisj 7443 cauappcvgprlemrnd 7570 caucvgprlemrnd 7593 caucvgprprlemrnd 7621 nn0n0n1ge2b 9243 fzind 9279 icoshft 9894 fzen 9945 seq3coll 10713 shftuz 10717 mulgcd 11900 algcvga 11928 lcmneg 11951 blssps 12838 blss 12839 metcnp3 12922 sincosq1sgn 13158 sincosq2sgn 13159 sincosq3sgn 13160 sincosq4sgn 13161 |
Copyright terms: Public domain | W3C validator |