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 1132 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 919 |
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 921 |
This theorem is referenced by: 3adant1l 1161 3adant1r 1162 3impdi 1224 vtocl3gf 2661 rspc2ev 2715 reuss 3245 trssord 4135 funtp 4972 resdif 5168 funimass4 5245 fnovex 5558 fnotovb 5568 fovrn 5663 fnovrn 5668 fmpt2co 5857 nndi 6088 nnaordi 6104 ecovass 6238 ecoviass 6239 ecovdi 6240 ecovidi 6241 eqsupti 6409 addasspig 6520 mulasspig 6522 distrpig 6523 distrnq0 6649 addassnq0 6652 distnq0r 6653 prcdnql 6674 prcunqu 6675 genpassl 6714 genpassu 6715 genpassg 6716 distrlem1prl 6772 distrlem1pru 6773 ltexprlemopl 6791 ltexprlemopu 6793 le2tri3i 7219 cnegexlem1 7283 subadd 7311 addsub 7319 subdi 7489 submul2 7503 div12ap 7782 diveqap1 7793 divnegap 7794 divdivap2 7812 ltmulgt11 7942 gt0div 7948 ge0div 7949 uzind3 8460 fnn0ind 8463 qdivcl 8728 irrmul 8732 xrlttr 8870 fzen 9062 iseqval 9440 lenegsq 9981 moddvds 10204 dvds2add 10229 dvds2sub 10230 dvdsleabs 10245 divalgb 10325 ndvdsadd 10331 modgcd 10382 absmulgcd 10406 |
Copyright terms: Public domain | W3C validator |