![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpanr2 | Structured version Visualization version 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 523 | . 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒)) |
3 | mpanr2.2 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
4 | 2, 3 | sylan2 591 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 395 |
This theorem is referenced by: fvreseq1 7047 op1steq 8038 fpmg 8887 pmresg 8889 pw2f1o 9102 pm54.43 10026 dfac2b 10155 ttukeylem6 10539 gruina 10843 muleqadd 11890 divdiv1 11958 addltmul 12481 elfzp1b 13613 elfzm1b 13614 expp1z 14112 expm1 14113 oddvdsnn0 19511 efgi0 19687 efgi1 19688 fiinbas 22899 opnneissb 23062 fclscf 23973 blssec 24385 iimulcl 24904 itg2lr 25704 blocnilem 30686 lnopmul 31849 opsqrlem6 32027 gsumle 32894 gsumvsca1 33025 gsumvsca2 33026 locfinreflem 33572 fvray 35868 fvline 35871 fneref 35965 poimirlem3 37227 poimirlem16 37240 fdc 37349 linepmap 39378 rmyeq0 42516 |
Copyright terms: Public domain | W3C validator |