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 1197 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 252 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 973 |
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 975 |
This theorem is referenced by: 3anidm12 1290 mob 2912 eqbrrdva 4781 funimaexglem 5281 fco 5363 f1oiso2 5806 caovimo 6046 smoel2 6282 nnaword 6490 3ecoptocl 6602 sbthlemi10 6943 distrnq0 7421 addassnq0 7424 prcdnql 7446 prcunqu 7447 genpdisj 7485 cauappcvgprlemrnd 7612 caucvgprlemrnd 7635 caucvgprprlemrnd 7663 nn0n0n1ge2b 9291 fzind 9327 icoshft 9947 fzen 9999 seq3coll 10777 shftuz 10781 mulgcd 11971 algcvga 12005 lcmneg 12028 isnmgm 12614 blssps 13221 blss 13222 metcnp3 13305 sincosq1sgn 13541 sincosq2sgn 13542 sincosq3sgn 13543 sincosq4sgn 13544 |
Copyright terms: Public domain | W3C validator |