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 698 | 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 206 df-an 397 |
This theorem is referenced by: mpanr12 702 oacl 8365 omcl 8366 oaordi 8377 oawordri 8381 oaass 8392 oarec 8393 omordi 8397 omwordri 8403 odi 8410 omass 8411 oeoelem 8429 undom 8846 fimax2g 9060 fimin2g 9256 frr1 9517 axcnre 10920 divdiv23zi 11728 recp1lt1 11873 divgt0i 11883 divge0i 11884 ltreci 11885 lereci 11886 lt2msqi 11887 le2msqi 11888 msq11i 11889 ltdiv23i 11899 ltdivp1i 11901 zmin 12684 ge0gtmnf 12906 hashprg 14110 sqrt11i 15096 sqrtmuli 15097 sqrtmsq2i 15099 sqrtlei 15100 sqrtlti 15101 cos01gt0 15900 wspthsnwspthsnon 28281 vc2OLD 28930 vc0 28936 vcm 28938 nvpi 29029 nvge0 29035 ipval3 29071 ipidsq 29072 sspmval 29095 opsqrlem1 30502 opsqrlem6 30507 hstle 30592 hstrbi 30628 atordi 30746 finorwe 35553 poimirlem6 35783 poimirlem7 35784 poimirlem16 35793 poimirlem19 35796 poimirlem20 35797 |
Copyright terms: Public domain | W3C validator |