![]() |
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 719 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan2 707 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 385 |
This theorem is referenced by: wfisg 5753 2dom 8070 limensuci 8177 phplem4 8183 unfi 8268 fiint 8278 cdaen 9033 isfin1-3 9246 prlem934 9893 0idsr 9956 1idsr 9957 00sr 9958 addresr 9997 mulresr 9998 reclt1 10956 crne0 11051 nominpos 11307 expnass 13010 faclbnd2 13118 crim 13899 sqrlem1 14027 sqrlem7 14033 sqrt00 14048 sqreulem 14143 mulcn2 14370 ege2le3 14864 sin02gt0 14966 opoe 15134 oddprm 15562 pythagtriplem2 15569 pythagtriplem3 15570 pythagtriplem16 15582 pythagtrip 15586 pc1 15607 prmlem0 15859 acsfn0 16368 mgpress 18546 abvneg 18882 pmatcollpw3 20637 leordtval2 21064 txswaphmeo 21656 iccntr 22671 dvlipcn 23802 sinq34lt0t 24306 cosordlem 24322 efif1olem3 24335 lgamgulmlem2 24801 basellem3 24854 ppiub 24974 bposlem9 25062 lgsne0 25105 lgsdinn0 25115 chebbnd1 25206 eupth2lem3lem4 27209 mayete3i 28715 lnop0 28953 nmcexi 29013 nmoptrii 29081 nmopcoadji 29088 hstle1 29213 hst0 29220 strlem5 29242 jplem1 29255 cnvoprabOLD 29626 subfacp1lem5 31292 frinsg 31870 limsucncmpi 32569 matunitlindflem1 33535 poimirlem15 33554 dvasin 33626 fdc 33671 eldioph3b 37645 sprsymrelfolem2 42068 sinhpcosh 42809 |
Copyright terms: Public domain | W3C validator |