![]() |
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 702 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan2 690 | 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: wfisgOLD 6352 f1ofvswap 7299 2dom 9026 limensuci 9149 phplem4OLD 9216 unfiOLD 9309 fiint 9320 frinsg 9742 djuen 10160 isfin1-3 10377 prlem934 11024 0idsr 11088 1idsr 11089 00sr 11090 addresr 11129 mulresr 11130 reclt1 12105 crne0 12201 nominpos 12445 expnass 14168 faclbnd2 14247 crim 15058 01sqrexlem1 15185 01sqrexlem7 15191 sqrt00 15206 sqreulem 15302 mulcn2 15536 ege2le3 16029 sin02gt0 16131 opoe 16302 oddprm 16739 pythagtriplem2 16746 pythagtriplem3 16747 pythagtriplem16 16759 pythagtrip 16763 pc1 16784 prmlem0 17035 acsfn0 17600 mgpress 19994 mgpressOLD 19995 abvneg 20430 pmatcollpw3 22268 leordtval2 22698 txswaphmeo 23291 iccntr 24319 dvlipcn 25493 sinq34lt0t 26001 cosordlem 26021 efif1olem3 26035 lgamgulmlem2 26514 basellem3 26567 ppiub 26687 bposlem9 26775 lgsne0 26818 lgsdinn0 26828 chebbnd1 26955 eupth2lem3lem4 29464 mayete3i 30959 lnop0 31197 nmcexi 31257 nmoptrii 31325 nmopcoadji 31332 hstle1 31457 hst0 31464 strlem5 31486 jplem1 31499 cnvoprabOLD 31923 subfacp1lem5 34113 limsucncmpi 35268 matunitlindflem1 36422 poimirlem15 36441 dvasin 36510 fdc 36551 eldioph3b 41436 oaabsb 41977 tfsconcatfv2 42023 or2expropbi 45679 ich2exprop 46074 sprsymrelfolem2 46096 sinhpcosh 47687 |
Copyright terms: Public domain | W3C validator |