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 362 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1160 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 947 |
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 949 |
This theorem is referenced by: 3adant1l 1193 3adant1r 1194 3impdi 1256 vtocl3gf 2723 rspc2ev 2778 reuss 3327 trssord 4272 funtp 5146 resdif 5357 funimass4 5440 fnovex 5772 fnotovb 5782 fovrn 5881 fnovrn 5886 fmpoco 6081 nndi 6350 nnaordi 6372 ecovass 6506 ecoviass 6507 ecovdi 6508 ecovidi 6509 eqsupti 6851 addasspig 7106 mulasspig 7108 distrpig 7109 distrnq0 7235 addassnq0 7238 distnq0r 7239 prcdnql 7260 prcunqu 7261 genpassl 7300 genpassu 7301 genpassg 7302 distrlem1prl 7358 distrlem1pru 7359 ltexprlemopl 7377 ltexprlemopu 7379 le2tri3i 7840 cnegexlem1 7905 subadd 7933 addsub 7941 subdi 8115 submul2 8129 div12ap 8421 diveqap1 8432 divnegap 8433 divdivap2 8451 ltmulgt11 8586 gt0div 8592 ge0div 8593 uzind3 9122 fnn0ind 9125 qdivcl 9391 irrmul 9395 xrlttr 9536 fzen 9778 lenegsq 10822 moddvds 11414 dvds2add 11439 dvds2sub 11440 dvdsleabs 11455 divalgb 11534 ndvdsadd 11540 modgcd 11591 absmulgcd 11617 setsresg 11908 unopn 12083 innei 12243 cncfi 12645 |
Copyright terms: Public domain | W3C validator |