| 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 524 | . 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒)) |
| 3 | mpanr2.2 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 4 | 2, 3 | sylan2 593 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: fvreseq1 6973 op1steq 7968 fpmg 8795 pmresg 8797 pw2f1o 8999 pm54.43 9897 dfac2b 10025 ttukeylem6 10408 gruina 10712 muleqadd 11764 divdiv1 11835 addltmul 12360 elfzp1b 13504 elfzm1b 13505 expp1z 14018 expm1 14019 oddvdsnn0 19423 efgi0 19599 efgi1 19600 gsumle 20024 fiinbas 22837 opnneissb 22999 fclscf 23910 blssec 24321 iimulcl 24831 itg2lr 25629 blocnilem 30748 lnopmul 31911 opsqrlem6 32089 gsumvsca1 33168 gsumvsca2 33169 locfinreflem 33807 fvray 36115 fvline 36118 fneref 36324 poimirlem3 37603 poimirlem16 37616 fdc 37725 linepmap 39754 rmyeq0 42926 omssaxinf2 44962 |
| Copyright terms: Public domain | W3C validator |