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 471 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 701 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: mpanr12 705 oacl 8184 omcl 8185 oaordi 8196 oawordri 8200 oaass 8211 oarec 8212 omordi 8216 omwordri 8222 odi 8229 omass 8230 oeoelem 8248 fimax2g 8831 fimin2g 9027 axcnre 10657 divdiv23zi 11464 recp1lt1 11609 divgt0i 11619 divge0i 11620 ltreci 11621 lereci 11622 lt2msqi 11623 le2msqi 11624 msq11i 11625 ltdiv23i 11635 ltdivp1i 11637 zmin 12419 ge0gtmnf 12641 hashprg 13841 sqrt11i 14827 sqrtmuli 14828 sqrtmsq2i 14830 sqrtlei 14831 sqrtlti 14832 cos01gt0 15629 wspthsnwspthsnon 27846 vc2OLD 28495 vc0 28501 vcm 28503 nvpi 28594 nvge0 28600 ipval3 28636 ipidsq 28637 sspmval 28660 opsqrlem1 30067 opsqrlem6 30072 hstle 30157 hstrbi 30193 atordi 30311 frr1 33454 finorwe 35165 poimirlem6 35395 poimirlem7 35396 poimirlem16 35405 poimirlem19 35408 poimirlem20 35409 |
Copyright terms: Public domain | W3C validator |