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 81 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
3 | 2 | imp 123 | . 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃)) |
4 | 3 | com12 30 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem is referenced by: impcomd 253 imp32 255 pm3.31 260 syland 291 imp4c 349 imp4d 350 imp5d 357 expimpd 361 expl 376 pm3.37 684 pm5.6r 922 3expib 1201 sbiedh 1780 equs5 1822 moexexdc 2103 rsp2 2520 moi 2913 reu6 2919 sbciegft 2985 prel12 3758 opthpr 3759 invdisj 3983 sowlin 4305 reusv1 4443 relop 4761 elres 4927 iss 4937 funssres 5240 fv3 5519 funfvima 5727 poxp 6211 tfri3 6346 nndi 6465 nnmass 6466 nnmordi 6495 nnmord 6496 eroveu 6604 fiintim 6906 suplubti 6977 addnq0mo 7409 mulnq0mo 7410 prcdnql 7446 prcunqu 7447 prnmaxl 7450 prnminu 7451 genprndl 7483 genprndu 7484 distrlem1prl 7544 distrlem1pru 7545 distrlem5prl 7548 distrlem5pru 7549 recexprlemss1l 7597 recexprlemss1u 7598 addsrmo 7705 mulsrmo 7706 mulgt0sr 7740 ltleletr 8001 mulgt1 8779 fzind 9327 eqreznegel 9573 fzen 9999 elfzodifsumelfzo 10157 bernneq 10596 mulcn2 11275 prodmodclem2 11540 dvdsmod0 11755 divalglemeunn 11880 divalglemeuneg 11882 ndvdssub 11889 algcvgblem 12003 coprmdvds 12046 coprmdvds2 12047 divgcdcoprm0 12055 pceu 12249 dvdsprmpweqnn 12289 oddprmdvds 12306 infpnlem1 12311 sgrpidmndm 12656 lmss 13040 lmtopcnp 13044 zabsle1 13694 bj-sbimedh 13806 bj-nnen2lp 13989 |
Copyright terms: Public domain | W3C validator |