![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpanl12 | Structured version Visualization version GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Ref | Expression |
---|---|
mpanl12.1 | ⊢ 𝜑 |
mpanl12.2 | ⊢ 𝜓 |
mpanl12.3 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mpanl12 | ⊢ (𝜒 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanl12.2 | . 2 ⊢ 𝜓 | |
2 | mpanl12.1 | . . 3 ⊢ 𝜑 | |
3 | mpanl12.3 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mpanl1 690 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 680 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: reuun1 4134 frminex 5335 tz6.26i 5965 wfii 5967 opthreg 8810 opthregOLD 8812 unsnen 9710 axcnre 10321 addgt0 10861 addgegt0 10862 addgtge0 10863 addge0 10864 addgt0i 10914 addge0i 10915 addgegt0i 10916 add20i 10918 mulge0i 10922 recextlem1 11005 recne0 11046 recdiv 11081 rec11i 11116 recgt1 11273 prodgt0i 11284 prodge0iOLD 11285 xadddi2 12439 iccshftri 12624 iccshftli 12626 iccdili 12628 icccntri 12630 mulexpz 13218 expaddz 13222 m1expeven 13225 iexpcyc 13288 cnpart 14387 resqrex 14398 sqreulem 14506 amgm2 14516 rlim 14634 ello12 14655 elo12 14666 ege2le3 15222 dvdslelem 15438 divalglem1 15524 divalglem6 15528 divalglem9 15531 gcdaddmlem 15651 sqnprm 15818 prmlem1 16213 prmlem2 16225 xpscfn 16605 m1expaddsub 18302 psgnuni 18303 gzrngunitlem 20207 lmres 21512 zdis 23027 iihalf1 23138 lmclimf 23510 vitali 23817 ismbf 23832 ismbfcn 23833 mbfconst 23837 cncombf 23862 cnmbf 23863 limcfval 24073 dvnfre 24152 quotlem 24492 ulmval 24571 ulmpm 24574 abelthlem2 24623 abelthlem3 24624 abelthlem5 24626 abelthlem7 24629 efcvx 24640 logtayl 24843 logccv 24846 cxpcn3 24929 emcllem2 25175 zetacvg 25193 basellem5 25263 bposlem7 25467 chebbnd1lem3 25612 dchrisumlem3 25632 iscgrgd 25864 axcontlem2 26314 nv1 28102 blocnilem 28231 ipasslem8 28264 siii 28280 ubthlem1 28298 norm1 28678 hhshsslem2 28697 hoscli 29193 hodcli 29194 cnlnadjlem7 29504 adjbdln 29514 pjnmopi 29579 strlem1 29681 rexdiv 30196 tpr2rico 30556 qqhre 30662 signsply0 31228 subfacval3 31770 erdszelem4 31775 erdszelem8 31779 elmrsubrn 32016 rdgprc 32288 frindi 32333 fwddifval 32858 fwddifnval 32859 poimirlem29 34048 ismblfin 34060 itg2addnclem 34070 caures 34164 |
Copyright terms: Public domain | W3C validator |