| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mpanr12 | Structured version Visualization version GIF version | ||
| Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.) |
| Ref | Expression |
|---|---|
| mpanr12.1 | ⊢ 𝜓 |
| mpanr12.2 | ⊢ 𝜒 |
| mpanr12.3 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
| Ref | Expression |
|---|---|
| mpanr12 | ⊢ (𝜑 → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpanr12.2 | . 2 ⊢ 𝜒 | |
| 2 | mpanr12.1 | . . 3 ⊢ 𝜓 | |
| 3 | mpanr12.3 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 4 | 2, 3 | mpanr1 703 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
| 5 | 1, 4 | mpan2 691 | 1 ⊢ (𝜑 → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: wfisgOLD 6375 f1ofvswap 7326 2dom 9070 limensuci 9193 phplem4OLD 9257 fiintOLD 9367 frinsg 9791 djuen 10210 isfin1-3 10426 prlem934 11073 0idsr 11137 1idsr 11138 00sr 11139 addresr 11178 mulresr 11179 reclt1 12163 crne0 12259 nominpos 12503 fvf1tp 13829 expnass 14247 faclbnd2 14330 crim 15154 01sqrexlem1 15281 01sqrexlem7 15287 sqrt00 15302 sqreulem 15398 mulcn2 15632 ege2le3 16126 sin02gt0 16228 opoe 16400 oddprm 16848 pythagtriplem2 16855 pythagtriplem3 16856 pythagtriplem16 16868 pythagtrip 16872 pc1 16893 prmlem0 17143 acsfn0 17703 mgpress 20147 abvneg 20827 pmatcollpw3 22790 leordtval2 23220 txswaphmeo 23813 iccntr 24843 dvlipcn 26033 sinq34lt0t 26551 cosordlem 26572 efif1olem3 26586 lgamgulmlem2 27073 basellem3 27126 ppiub 27248 bposlem9 27336 lgsne0 27379 lgsdinn0 27389 chebbnd1 27516 eupth2lem3lem4 30250 mayete3i 31747 lnop0 31985 nmcexi 32045 nmoptrii 32113 nmopcoadji 32120 hstle1 32245 hst0 32252 strlem5 32274 jplem1 32287 subfacp1lem5 35189 limsucncmpi 36446 matunitlindflem1 37623 poimirlem15 37642 dvasin 37711 fdc 37752 eldioph3b 42776 oaabsb 43307 tfsconcatfv2 43353 omssaxinf2 45005 or2expropbi 47046 ich2exprop 47458 sprsymrelfolem2 47480 clnbgrisubgrgrim 47900 sinhpcosh 49259 |
| Copyright terms: Public domain | W3C validator |