![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impd | GIF version |
Description: Importation deduction. (Contributed by NM, 31-Mar-1994.) |
Ref | Expression |
---|---|
imp3.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
impd | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp3.1 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
2 | 1 | com3l 80 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
3 | 2 | imp 122 | . 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃)) |
4 | 3 | com12 30 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 |
This theorem is referenced by: imp32 253 pm3.31 258 syland 287 imp4c 343 imp4d 344 imp5d 351 expimpd 355 expl 370 pm3.37 822 pm5.6r 870 3expib 1142 sbiedh 1711 equs5 1751 moexexdc 2026 rsp2 2414 moi 2776 reu6 2782 sbciegft 2845 prel12 3571 opthpr 3572 invdisj 3788 sowlin 4083 reusv1 4216 relop 4514 elres 4674 iss 4684 funssres 4972 fv3 5229 funfvima 5422 poxp 5884 tfri3 6016 nndi 6130 nnmass 6131 nnmordi 6155 nnmord 6156 eroveu 6263 suplubti 6472 addnq0mo 6699 mulnq0mo 6700 prcdnql 6736 prcunqu 6737 prnmaxl 6740 prnminu 6741 genprndl 6773 genprndu 6774 distrlem1prl 6834 distrlem1pru 6835 distrlem5prl 6838 distrlem5pru 6839 recexprlemss1l 6887 recexprlemss1u 6888 addsrmo 6982 mulsrmo 6983 mulgt0sr 7016 ltleletr 7260 mulgt1 8008 fzind 8543 eqreznegel 8780 fzen 9138 elfzodifsumelfzo 9287 bernneq 9690 mulcn2 10289 divalglemeunn 10465 divalglemeuneg 10467 ndvdssub 10474 algcvgblem 10575 coprmdvds 10618 coprmdvds2 10619 divgcdcoprm0 10627 bj-sbimedh 10733 bj-nnen2lp 10907 |
Copyright terms: Public domain | W3C validator |