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 468 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 697 | 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: mpanr12 701 oacl 8149 omcl 8150 oaordi 8161 oawordri 8165 oaass 8176 oarec 8177 omordi 8181 omwordri 8187 odi 8194 omass 8195 oeoelem 8213 fimax2g 8752 fimin2g 8949 axcnre 10574 divdiv23zi 11381 recp1lt1 11526 divgt0i 11536 divge0i 11537 ltreci 11538 lereci 11539 lt2msqi 11540 le2msqi 11541 msq11i 11542 ltdiv23i 11552 ltdivp1i 11554 zmin 12332 ge0gtmnf 12553 hashprg 13744 sqrt11i 14732 sqrtmuli 14733 sqrtmsq2i 14735 sqrtlei 14736 sqrtlti 14737 cos01gt0 15532 wspthsnwspthsnon 27622 vc2OLD 28272 vc0 28278 vcm 28280 nvpi 28371 nvge0 28377 ipval3 28413 ipidsq 28414 sspmval 28437 opsqrlem1 29844 opsqrlem6 29849 hstle 29934 hstrbi 29970 atordi 30088 frr1 33041 finorwe 34545 poimirlem6 34779 poimirlem7 34780 poimirlem16 34789 poimirlem19 34792 poimirlem20 34793 |
Copyright terms: Public domain | W3C validator |