| 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 700 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
| 5 | 1, 4 | mpan 690 | 1 ⊢ (𝜒 → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: reuun1 4328 frminex 5664 tz6.26i 6370 wfii 6373 wfr3OLD 8378 tfr2ALT 8441 tfr3ALT 8442 opthreg 9658 unsnen 10593 axcnre 11204 addgt0 11749 addgegt0 11750 addgtge0 11751 addge0 11752 addgt0i 11802 addge0i 11803 addgegt0i 11804 add20i 11806 mulge0i 11810 recextlem1 11893 recne0 11935 recdiv 11973 rec11i 12008 recgt1 12164 prodgt0i 12175 xadddi2 13339 iccshftri 13527 iccshftli 13529 iccdili 13531 icccntri 13533 mulexpz 14143 expaddz 14147 m1expeven 14150 iexpcyc 14246 cnpart 15279 resqrex 15289 sqreulem 15398 amgm2 15408 rlim 15531 ello12 15552 elo12 15563 bpolylem 16084 ege2le3 16126 dvdslelem 16346 divalglem1 16431 divalglem6 16435 divalglem9 16438 gcdaddmlem 16561 sqnprm 16739 prmlem1 17145 prmlem2 17157 m1expaddsub 19516 psgnuni 19517 gzrngunitlem 21450 lmres 23308 zdis 24838 iihalf1 24958 lmclimf 25338 vitali 25648 ismbf 25663 ismbfcn 25664 mbfconst 25668 cncombf 25693 cnmbf 25694 limcfval 25907 dvnfre 25990 quotlem 26342 ulmval 26423 ulmpm 26426 abelthlem2 26476 abelthlem3 26477 abelthlem5 26479 abelthlem7 26482 efcvx 26493 logtayl 26702 logccv 26705 cxpcn3 26791 emcllem2 27040 zetacvg 27058 basellem5 27128 bposlem7 27334 chebbnd1lem3 27515 dchrisumlem3 27535 iscgrgd 28521 axcontlem2 28980 nv1 30694 blocnilem 30823 ipasslem8 30856 siii 30872 ubthlem1 30889 norm1 31268 hhshsslem2 31287 hoscli 31781 hodcli 31782 cnlnadjlem7 32092 adjbdln 32102 pjnmopi 32167 strlem1 32269 rexdiv 32908 tpr2rico 33911 qqhre 34021 signsply0 34566 subfacval3 35194 erdszelem4 35199 erdszelem8 35203 elmrsubrn 35525 rdgprc 35795 fwddifval 36163 fwddifnval 36164 exrecfnlem 37380 poimirlem29 37656 ismblfin 37668 itg2addnclem 37678 caures 37767 sswfaxreg 45004 iooii 48815 icccldii 48816 |
| Copyright terms: Public domain | W3C validator |