![]() |
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 698 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 688 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: reuun1 4317 frminex 5658 tz6.26i 6357 wfii 6360 wfr3OLD 8359 tfr2ALT 8422 tfr3ALT 8423 opthreg 9643 unsnen 10578 axcnre 11189 addgt0 11732 addgegt0 11733 addgtge0 11734 addge0 11735 addgt0i 11785 addge0i 11786 addgegt0i 11787 add20i 11789 mulge0i 11793 recextlem1 11876 recne0 11918 recdiv 11953 rec11i 11988 recgt1 12143 prodgt0i 12154 xadddi2 13311 iccshftri 13499 iccshftli 13501 iccdili 13503 icccntri 13505 mulexpz 14103 expaddz 14107 m1expeven 14110 iexpcyc 14206 cnpart 15223 resqrex 15233 sqreulem 15342 amgm2 15352 rlim 15475 ello12 15496 elo12 15507 bpolylem 16028 ege2le3 16070 dvdslelem 16289 divalglem1 16374 divalglem6 16378 divalglem9 16381 gcdaddmlem 16502 sqnprm 16676 prmlem1 17080 prmlem2 17092 m1expaddsub 19465 psgnuni 19466 gzrngunitlem 21382 lmres 23248 zdis 24776 iihalf1 24896 lmclimf 25276 vitali 25586 ismbf 25601 ismbfcn 25602 mbfconst 25606 cncombf 25631 cnmbf 25632 limcfval 25845 dvnfre 25928 quotlem 26280 ulmval 26361 ulmpm 26364 abelthlem2 26414 abelthlem3 26415 abelthlem5 26417 abelthlem7 26420 efcvx 26431 logtayl 26639 logccv 26642 cxpcn3 26728 emcllem2 26974 zetacvg 26992 basellem5 27062 bposlem7 27268 chebbnd1lem3 27449 dchrisumlem3 27469 iscgrgd 28389 axcontlem2 28848 nv1 30557 blocnilem 30686 ipasslem8 30719 siii 30735 ubthlem1 30752 norm1 31131 hhshsslem2 31150 hoscli 31644 hodcli 31645 cnlnadjlem7 31955 adjbdln 31965 pjnmopi 32030 strlem1 32132 rexdiv 32734 tpr2rico 33644 qqhre 33752 signsply0 34314 subfacval3 34930 erdszelem4 34935 erdszelem8 34939 elmrsubrn 35261 rdgprc 35521 fwddifval 35889 fwddifnval 35890 exrecfnlem 36989 poimirlem29 37253 ismblfin 37265 itg2addnclem 37275 caures 37364 iooii 48122 icccldii 48123 |
Copyright terms: Public domain | W3C validator |