![]() |
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 6469 op1steq 7365 fpmg 8037 pmresg 8039 pw2f1o 8218 pm54.43 8987 dfac2b 9114 dfac2OLD 9116 ttukeylem6 9499 gruina 9803 muleqadd 10834 divdiv1 10899 addltmul 11431 elfzp1b 12581 elfzm1b 12582 expp1z 13074 expm1 13075 oddvdsnn0 18134 efgi0 18304 efgi1 18305 fiinbas 20929 opnneissb 21091 fclscf 22001 blssec 22412 iimulcl 22908 itg2lr 23667 blocnilem 27939 lnopmul 29106 opsqrlem6 29284 gsumle 30059 gsumvsca1 30062 gsumvsca2 30063 locfinreflem 30187 fvray 32525 fvline 32528 fneref 32622 poimirlem3 33694 poimirlem16 33707 fdc 33823 linepmap 35533 rmyeq0 37991 |
Copyright terms: Public domain | W3C validator |