![]() |
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 469 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 700 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: mpanr12 704 oacl 8530 omcl 8531 oaordi 8542 oawordri 8546 oaass 8557 oarec 8558 omordi 8562 omwordri 8568 odi 8575 omass 8576 oeoelem 8594 undom 9055 fimax2g 9285 fimin2g 9488 frr1 9750 axcnre 11155 divdiv23zi 11963 recp1lt1 12108 divgt0i 12118 divge0i 12119 ltreci 12120 lereci 12121 lt2msqi 12122 le2msqi 12123 msq11i 12124 ltdiv23i 12134 ltdivp1i 12136 zmin 12924 ge0gtmnf 13147 hashprg 14351 sqrt11i 15327 sqrtmuli 15328 sqrtmsq2i 15330 sqrtlei 15331 sqrtlti 15332 cos01gt0 16130 wspthsnwspthsnon 29150 vc2OLD 29799 vc0 29805 vcm 29807 nvpi 29898 nvge0 29904 ipval3 29940 ipidsq 29941 sspmval 29964 opsqrlem1 31371 opsqrlem6 31376 hstle 31461 hstrbi 31497 atordi 31615 finorwe 36201 poimirlem6 36432 poimirlem7 36433 poimirlem16 36442 poimirlem19 36445 poimirlem20 36446 |
Copyright terms: Public domain | W3C validator |