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 699 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan2 687 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: wfisg 6176 2dom 8570 limensuci 8681 phplem4 8687 unfi 8773 fiint 8783 djuen 9583 isfin1-3 9796 prlem934 10443 0idsr 10507 1idsr 10508 00sr 10509 addresr 10548 mulresr 10549 reclt1 11523 crne0 11619 nominpos 11862 expnass 13558 faclbnd2 13639 crim 14462 sqrlem1 14590 sqrlem7 14596 sqrt00 14611 sqreulem 14707 mulcn2 14940 ege2le3 15431 sin02gt0 15533 opoe 15700 oddprm 16135 pythagtriplem2 16142 pythagtriplem3 16143 pythagtriplem16 16155 pythagtrip 16159 pc1 16180 prmlem0 16427 acsfn0 16919 mgpress 19179 abvneg 19534 pmatcollpw3 21320 leordtval2 21748 txswaphmeo 22341 iccntr 23356 dvlipcn 24518 sinq34lt0t 25022 cosordlem 25042 efif1olem3 25055 lgamgulmlem2 25534 basellem3 25587 ppiub 25707 bposlem9 25795 lgsne0 25838 lgsdinn0 25848 chebbnd1 25975 eupth2lem3lem4 27937 mayete3i 29432 lnop0 29670 nmcexi 29730 nmoptrii 29798 nmopcoadji 29805 hstle1 29930 hst0 29937 strlem5 29959 jplem1 29972 cnvoprabOLD 30382 subfacp1lem5 32328 frinsg 32984 limsucncmpi 33690 matunitlindflem1 34769 poimirlem15 34788 dvasin 34859 fdc 34901 eldioph3b 39240 or2expropbi 43146 ich2exprop 43510 sprsymrelfolem2 43532 sinhpcosh 44767 |
Copyright terms: Public domain | W3C validator |