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 678 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 713 | 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 196 df-an 385 |
This theorem is referenced by: mpanr12 717 oacl 7502 omcl 7503 oaordi 7513 oawordri 7517 oaass 7528 oarec 7529 omordi 7533 omwordri 7539 odi 7546 omass 7547 oeoelem 7565 fimax2g 8091 fimin2g 8286 axcnre 9864 divdiv23zi 10657 recp1lt1 10800 divgt0i 10811 divge0i 10812 ltreci 10813 lereci 10814 lt2msqi 10815 le2msqi 10816 msq11i 10817 ltdiv23i 10827 ltdivp1i 10829 zmin 11660 ge0gtmnf 11877 hashprg 13043 hashprgOLD 13044 sqrt11i 13972 sqrtmuli 13973 sqrtmsq2i 13975 sqrtlei 13976 sqrtlti 13977 cos01gt0 14760 0wlk 26075 0trl 26076 0pth 26100 0spth 26101 0crct 26154 0cycl 26155 0clwlk 26293 vc2OLD 26807 vc0 26813 vcm 26815 nvpi 26906 nvge0 26912 ipval3 26948 ipidsq 26949 sspmval 26972 opsqrlem1 28383 opsqrlem6 28388 hstle 28473 hstrbi 28509 atordi 28627 poimirlem6 32585 poimirlem7 32586 poimirlem16 32595 poimirlem19 32598 poimirlem20 32599 |
Copyright terms: Public domain | W3C validator |