![]() |
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 1203 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 254 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 981 |
This theorem is referenced by: 3anidm12 1305 mob 2931 eqbrrdva 4809 funimaexglem 5311 fco 5393 f1oiso2 5841 caovimo 6082 smoel2 6318 nnaword 6526 3ecoptocl 6638 sbthlemi10 6979 distrnq0 7472 addassnq0 7475 prcdnql 7497 prcunqu 7498 genpdisj 7536 cauappcvgprlemrnd 7663 caucvgprlemrnd 7686 caucvgprprlemrnd 7714 nn0n0n1ge2b 9346 fzind 9382 icoshft 10004 fzen 10057 seq3coll 10836 shftuz 10840 mulgcd 12031 algcvga 12065 lcmneg 12088 isnmgm 12798 issgrpd 12837 iscmnd 13192 unitmulclb 13419 rmodislmodlem 13596 rmodislmod 13597 blssps 14280 blss 14281 metcnp3 14364 sincosq1sgn 14600 sincosq2sgn 14601 sincosq3sgn 14602 sincosq4sgn 14603 |
Copyright terms: Public domain | W3C validator |