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 680 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 717 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 386 |
This theorem is referenced by: mpanr12 721 oacl 7615 omcl 7616 oaordi 7626 oawordri 7630 oaass 7641 oarec 7642 omordi 7646 omwordri 7652 odi 7659 omass 7660 oeoelem 7678 fimax2g 8206 fimin2g 8403 axcnre 9985 divdiv23zi 10778 recp1lt1 10921 divgt0i 10932 divge0i 10933 ltreci 10934 lereci 10935 lt2msqi 10936 le2msqi 10937 msq11i 10938 ltdiv23i 10948 ltdivp1i 10950 zmin 11784 ge0gtmnf 12003 hashprg 13182 hashprgOLD 13183 sqrt11i 14124 sqrtmuli 14125 sqrtmsq2i 14127 sqrtlei 14128 sqrtlti 14129 cos01gt0 14921 vc2OLD 27423 vc0 27429 vcm 27431 nvpi 27522 nvge0 27528 ipval3 27564 ipidsq 27565 sspmval 27588 opsqrlem1 28999 opsqrlem6 29004 hstle 29089 hstrbi 29125 atordi 29243 poimirlem6 33415 poimirlem7 33416 poimirlem16 33425 poimirlem19 33428 poimirlem20 33429 |
Copyright terms: Public domain | W3C validator |