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 267 | . 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃)) |
4 | 1, 3 | mpan2d 424 | 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 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpani 426 mp2and 429 rspcimedv 2765 ovig 5860 prcdnql 7260 prcunqu 7261 p1le 8575 nnge1 8711 zltp1le 9076 gtndiv 9114 uzss 9314 addlelt 9523 xrre2 9572 xrre3 9573 zltaddlt1le 9757 modfzo0difsn 10136 leexp2r 10315 expnlbnd2 10385 facavg 10460 caubnd2 10857 maxleast 10953 mulcn2 11049 cn1lem 11051 climsqz 11072 climsqz2 11073 climcvg1nlem 11086 fsumabs 11202 cvgratnnlemnexp 11261 cvgratnnlemmn 11262 zsupcllemstep 11565 gcdzeq 11637 algcvgblem 11657 algcvga 11659 lcmdvdsb 11692 coprm 11749 bldisj 12497 xblm 12513 metss2lem 12593 bdxmet 12597 limccoap 12743 |
Copyright terms: Public domain | W3C validator |