![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3impb | GIF version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impb.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
3impb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impb.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
2 | 1 | exp32 357 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1133 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: 3adant1l 1162 3adant1r 1163 3impdi 1225 vtocl3gf 2672 rspc2ev 2725 reuss 3263 trssord 4171 funtp 5020 resdif 5223 funimass4 5300 fnovex 5617 fnotovb 5627 fovrn 5722 fnovrn 5727 fmpt2co 5916 nndi 6179 nnaordi 6197 ecovass 6331 ecoviass 6332 ecovdi 6333 ecovidi 6334 eqsupti 6598 addasspig 6792 mulasspig 6794 distrpig 6795 distrnq0 6921 addassnq0 6924 distnq0r 6925 prcdnql 6946 prcunqu 6947 genpassl 6986 genpassu 6987 genpassg 6988 distrlem1prl 7044 distrlem1pru 7045 ltexprlemopl 7063 ltexprlemopu 7065 le2tri3i 7496 cnegexlem1 7560 subadd 7588 addsub 7596 subdi 7766 submul2 7780 div12ap 8059 diveqap1 8070 divnegap 8071 divdivap2 8089 ltmulgt11 8219 gt0div 8225 ge0div 8226 uzind3 8755 fnn0ind 8758 qdivcl 9023 irrmul 9027 xrlttr 9160 fzen 9352 iseqval 9749 lenegsq 10355 moddvds 10585 dvds2add 10610 dvds2sub 10611 dvdsleabs 10626 divalgb 10705 ndvdsadd 10711 modgcd 10762 absmulgcd 10786 |
Copyright terms: Public domain | W3C validator |