![]() |
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 525 | . 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒)) |
3 | mpanr2.2 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
4 | 2, 3 | sylan2 592 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: fvreseq1 6681 op1steq 7596 fpmg 8289 pmresg 8291 pw2f1o 8476 pm54.43 9282 dfac2b 9409 ttukeylem6 9789 gruina 10093 muleqadd 11138 divdiv1 11205 addltmul 11727 elfzp1b 12838 elfzm1b 12839 expp1z 13332 expm1 13333 oddvdsnn0 18407 efgi0 18577 efgi1 18578 fiinbas 21248 opnneissb 21410 fclscf 22321 blssec 22732 iimulcl 23228 itg2lr 24018 blocnilem 28268 lnopmul 29431 opsqrlem6 29609 gsumle 30490 gsumvsca1 30493 gsumvsca2 30494 locfinreflem 30717 fvray 33213 fvline 33216 fneref 33309 poimirlem3 34447 poimirlem16 34460 fdc 34573 linepmap 36463 rmyeq0 39056 |
Copyright terms: Public domain | W3C validator |