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 8422 diveqap1 8433 divnegap 8434 divdivap2 8452 ltmulgt11 8590 gt0div 8596 ge0div 8597 uzind3 9132 fnn0ind 9135 qdivcl 9403 irrmul 9407 xrlttr 9549 fzen 9791 lenegsq 10835 moddvds 11429 dvds2add 11454 dvds2sub 11455 dvdsleabs 11470 divalgb 11549 ndvdsadd 11555 modgcd 11606 absmulgcd 11632 setsresg 11924 unopn 12099 innei 12259 cncfi 12661 |
Copyright terms: Public domain | W3C validator |