![]() |
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 365 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1194 | 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: 3adant1l 1231 3adant1r 1232 3impdi 1303 vtocl3gf 2812 rspc2ev 2868 reuss 3428 trssord 4392 funtp 5281 resdif 5495 funimass4 5579 fnovex 5921 fnotovb 5931 fovcdm 6031 fnovrn 6036 fmpoco 6231 nndi 6501 nnaordi 6523 ecovass 6658 ecoviass 6659 ecovdi 6660 ecovidi 6661 eqsupti 7009 addasspig 7343 mulasspig 7345 distrpig 7346 distrnq0 7472 addassnq0 7475 distnq0r 7476 prcdnql 7497 prcunqu 7498 genpassl 7537 genpassu 7538 genpassg 7539 distrlem1prl 7595 distrlem1pru 7596 ltexprlemopl 7614 ltexprlemopu 7616 le2tri3i 8080 cnegexlem1 8146 subadd 8174 addsub 8182 subdi 8356 submul2 8370 div12ap 8665 diveqap1 8676 divnegap 8677 divdivap2 8695 ltmulgt11 8835 gt0div 8841 ge0div 8842 uzind3 9380 fnn0ind 9383 qdivcl 9657 irrmul 9661 xrlttr 9809 fzen 10057 lenegsq 11118 moddvds 11820 dvds2add 11846 dvds2sub 11847 dvdsleabs 11865 divalgb 11944 ndvdsadd 11950 modgcd 12006 absmulgcd 12032 odzval 12255 pcmul 12315 setsresg 12514 issubmnd 12865 submcl 12892 grpinvid1 12949 grpinvid2 12950 mulgp1 13048 cmncom 13139 islss3 13568 unopn 13801 innei 13959 cncfi 14361 |
Copyright terms: Public domain | W3C validator |