![]() |
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 566 | . 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒)) |
3 | mpanr2.2 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
4 | 2, 3 | sylan2 492 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: fvreseq1 6482 op1steq 7378 fpmg 8051 pmresg 8053 pw2f1o 8232 pm54.43 9036 dfac2b 9163 dfac2OLD 9165 ttukeylem6 9548 gruina 9852 muleqadd 10883 divdiv1 10948 addltmul 11480 elfzp1b 12630 elfzm1b 12631 expp1z 13123 expm1 13124 oddvdsnn0 18183 efgi0 18353 efgi1 18354 fiinbas 20978 opnneissb 21140 fclscf 22050 blssec 22461 iimulcl 22957 itg2lr 23716 blocnilem 27989 lnopmul 29156 opsqrlem6 29334 gsumle 30109 gsumvsca1 30112 gsumvsca2 30113 locfinreflem 30237 fvray 32575 fvline 32578 fneref 32672 poimirlem3 33743 poimirlem16 33756 fdc 33872 linepmap 35582 rmyeq0 38040 |
Copyright terms: Public domain | W3C validator |