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 715 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan2 703 | 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 196 df-an 385 |
This theorem is referenced by: wfisg 5632 2dom 7915 limensuci 8021 phplem4 8027 unfi 8112 fiint 8122 cdaen 8878 isfin1-3 9091 prlem934 9734 0idsr 9797 1idsr 9798 00sr 9799 addresr 9838 mulresr 9839 reclt1 10797 crne0 10890 nominpos 11146 expnass 12832 faclbnd2 12940 crim 13703 sqrlem1 13831 sqrlem7 13837 sqrt00 13852 sqreulem 13947 mulcn2 14174 ege2le3 14659 sin02gt0 14761 opoe 14925 oddprm 15353 pythagtriplem2 15360 pythagtriplem3 15361 pythagtriplem16 15373 pythagtrip 15377 pc1 15398 prmlem0 15650 acsfn0 16144 mgpress 18323 abvneg 18657 pmatcollpw3 20408 leordtval2 20826 txswaphmeo 21418 iccntr 22432 dvlipcn 23561 sinq34lt0t 24065 cosordlem 24081 efif1olem3 24094 lgamgulmlem2 24556 basellem3 24609 ppiub 24729 bposlem9 24817 lgsne0 24860 lgsdinn0 24870 chebbnd1 24961 constr1trl 26118 constr2trl 26129 usgrcyclnl2 26169 4cycl4dv 26195 2spontn0vne 26414 eupath2lem3 26506 mayete3i 27971 lnop0 28209 nmcexi 28269 nmoptrii 28337 nmopcoadji 28344 hstle1 28469 hst0 28476 strlem5 28498 jplem1 28511 cnvoprab 28886 subfacp1lem5 30420 frinsg 30986 limsucncmpi 31614 matunitlindflem1 32575 poimirlem15 32594 dvasin 32666 fdc 32711 eldioph3b 36346 eupth2lem3lem4 41399 sinhpcosh 42280 |
Copyright terms: Public domain | W3C validator |