![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpand | GIF version |
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpand.1 | ⊢ (𝜑 → 𝜓) |
mpand.2 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Ref | Expression |
---|---|
mpand | ⊢ (𝜑 → (𝜒 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpand.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | mpand.2 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
3 | 2 | ancomsd 269 | . 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃)) |
4 | 1, 3 | mpan2d 428 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
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 |
This theorem is referenced by: mpani 430 mp2and 433 rspcimedv 2843 ovig 5995 prcdnql 7482 prcunqu 7483 p1le 8805 nnge1 8941 zltp1le 9306 gtndiv 9347 uzss 9547 addlelt 9767 xrre2 9820 xrre3 9821 zltaddlt1le 10006 modfzo0difsn 10394 leexp2r 10573 expnlbnd2 10645 facavg 10725 caubnd2 11125 maxleast 11221 mulcn2 11319 cn1lem 11321 climsqz 11342 climsqz2 11343 climcvg1nlem 11356 fsumabs 11472 cvgratnnlemnexp 11531 cvgratnnlemmn 11532 zsupcllemstep 11945 gcdzeq 12022 algcvgblem 12048 algcvga 12050 lcmdvdsb 12083 coprm 12143 pclemub 12286 bldisj 13837 xblm 13853 metss2lem 13933 bdxmet 13937 limccoap 14083 lgsne0 14375 |
Copyright terms: Public domain | W3C validator |