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 696 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 686 | 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: reuun1 4284 frminex 5529 tz6.26i 6174 wfii 6176 opthreg 9070 unsnen 9964 axcnre 10575 addgt0 11115 addgegt0 11116 addgtge0 11117 addge0 11118 addgt0i 11168 addge0i 11169 addgegt0i 11170 add20i 11172 mulge0i 11176 recextlem1 11259 recne0 11300 recdiv 11335 rec11i 11370 recgt1 11525 prodgt0i 11536 xadddi2 12680 iccshftri 12863 iccshftli 12865 iccdili 12867 icccntri 12869 mulexpz 13459 expaddz 13463 m1expeven 13466 iexpcyc 13559 cnpart 14589 resqrex 14600 sqreulem 14709 amgm2 14719 rlim 14842 ello12 14863 elo12 14874 ege2le3 15433 dvdslelem 15649 divalglem1 15735 divalglem6 15739 divalglem9 15742 gcdaddmlem 15862 sqnprm 16036 prmlem1 16431 prmlem2 16443 m1expaddsub 18557 psgnuni 18558 gzrngunitlem 20540 lmres 21838 zdis 23353 iihalf1 23464 lmclimf 23836 vitali 24143 ismbf 24158 ismbfcn 24159 mbfconst 24163 cncombf 24188 cnmbf 24189 limcfval 24399 dvnfre 24478 quotlem 24818 ulmval 24897 ulmpm 24900 abelthlem2 24949 abelthlem3 24950 abelthlem5 24952 abelthlem7 24955 efcvx 24966 logtayl 25170 logccv 25173 cxpcn3 25256 emcllem2 25502 zetacvg 25520 basellem5 25590 bposlem7 25794 chebbnd1lem3 25975 dchrisumlem3 25995 iscgrgd 26227 axcontlem2 26679 nv1 28380 blocnilem 28509 ipasslem8 28542 siii 28558 ubthlem1 28575 norm1 28954 hhshsslem2 28973 hoscli 29467 hodcli 29468 cnlnadjlem7 29778 adjbdln 29788 pjnmopi 29853 strlem1 29955 rexdiv 30530 tpr2rico 31055 qqhre 31161 signsply0 31721 subfacval3 32334 erdszelem4 32339 erdszelem8 32343 elmrsubrn 32665 rdgprc 32937 frindi 32984 fwddifval 33521 fwddifnval 33522 exrecfnlem 34543 poimirlem29 34803 ismblfin 34815 itg2addnclem 34825 caures 34918 |
Copyright terms: Public domain | W3C validator |