|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > mpanr1 | 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.) | 
| Ref | Expression | 
|---|---|
| mpanr1.1 | ⊢ 𝜓 | 
| mpanr1.2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | 
| Ref | Expression | 
|---|---|
| mpanr1 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | mpanr1.1 | . 2 ⊢ 𝜓 | |
| 2 | mpanr1.2 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 3 | 2 | anassrs 467 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | 
| 4 | 1, 3 | mpanl2 701 | 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: mpanr12 705 oacl 8574 omcl 8575 oaordi 8585 oawordri 8589 oaass 8600 oarec 8601 omordi 8605 omwordri 8611 odi 8618 omass 8619 oeoelem 8637 undom 9100 fimax2g 9323 fimin2g 9538 frr1 9800 axcnre 11205 divdiv23zi 12021 recp1lt1 12167 divgt0i 12177 divge0i 12178 ltreci 12179 lereci 12180 lt2msqi 12181 le2msqi 12182 msq11i 12183 ltdiv23i 12193 ltdivp1i 12195 zmin 12987 ge0gtmnf 13215 hashprg 14435 sqrt11i 15424 sqrtmuli 15425 sqrtmsq2i 15427 sqrtlei 15428 sqrtlti 15429 cos01gt0 16228 wspthsnwspthsnon 29937 vc2OLD 30588 vc0 30594 vcm 30596 nvpi 30687 nvge0 30693 ipval3 30729 ipidsq 30730 sspmval 30753 opsqrlem1 32160 opsqrlem6 32165 hstle 32250 hstrbi 32286 atordi 32404 weiunlem2 36465 finorwe 37384 poimirlem6 37634 poimirlem7 37635 poimirlem16 37644 poimirlem19 37647 poimirlem20 37648 | 
| Copyright terms: Public domain | W3C validator |