![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpanr2 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpanr2.1 | ⊢ 𝜒 |
mpanr2.2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
mpanr2 | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanr2.1 | . . 3 ⊢ 𝜒 | |
2 | 1 | jctr 315 | . 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒)) |
3 | mpanr2.2 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
4 | 2, 3 | sylan2 286 | 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 is referenced by: op1steq 6204 fpmg 6700 pmresg 6702 pw2f1odc 6863 pm54.43 7219 prarloclemarch2 7448 prarloclemlt 7522 prsradd 7815 muleqadd 8655 divdivap1 8710 addltmul 9185 elfzp1b 10127 elfzm1b 10128 expp1zap 10600 expm1ap 10601 fiinbas 14006 opnneissb 14112 blssec 14395 |
Copyright terms: Public domain | W3C validator |