|   | 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 7058 op1steq 8059 fpmg 8909 pmresg 8911 pw2f1o 9118 pm54.43 10042 dfac2b 10172 ttukeylem6 10555 gruina 10859 muleqadd 11908 divdiv1 11979 addltmul 12504 elfzp1b 13642 elfzm1b 13643 expp1z 14153 expm1 14154 oddvdsnn0 19563 efgi0 19739 efgi1 19740 fiinbas 22960 opnneissb 23123 fclscf 24034 blssec 24446 iimulcl 24967 itg2lr 25766 blocnilem 30824 lnopmul 31987 opsqrlem6 32165 gsumle 33102 gsumvsca1 33233 gsumvsca2 33234 locfinreflem 33840 fvray 36143 fvline 36146 fneref 36352 poimirlem3 37631 poimirlem16 37644 fdc 37753 linepmap 39778 rmyeq0 42970 omssaxinf2 45010 | 
| Copyright terms: Public domain | W3C validator |