![]() |
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 681 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 717 | 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: mpanr12 721 oacl 7660 omcl 7661 oaordi 7671 oawordri 7675 oaass 7686 oarec 7687 omordi 7691 omwordri 7697 odi 7704 omass 7705 oeoelem 7723 fimax2g 8247 fimin2g 8444 axcnre 10023 divdiv23zi 10816 recp1lt1 10959 divgt0i 10970 divge0i 10971 ltreci 10972 lereci 10973 lt2msqi 10974 le2msqi 10975 msq11i 10976 ltdiv23i 10986 ltdivp1i 10988 zmin 11822 ge0gtmnf 12041 hashprg 13220 hashprgOLD 13221 sqrt11i 14168 sqrtmuli 14169 sqrtmsq2i 14171 sqrtlei 14172 sqrtlti 14173 cos01gt0 14965 wspthsnwspthsnon 26879 vc2OLD 27551 vc0 27557 vcm 27559 nvpi 27650 nvge0 27656 ipval3 27692 ipidsq 27693 sspmval 27716 opsqrlem1 29127 opsqrlem6 29132 hstle 29217 hstrbi 29253 atordi 29371 poimirlem6 33545 poimirlem7 33546 poimirlem16 33555 poimirlem19 33558 poimirlem20 33559 |
Copyright terms: Public domain | W3C validator |