![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > impl | Structured version Visualization version GIF version |
Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.) |
Ref | Expression |
---|---|
impl.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Ref | Expression |
---|---|
impl | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impl.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
2 | 1 | expd 416 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp31 418 | 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 206 df-an 397 |
This theorem is referenced by: sbc2iedv 3858 csbie2t 3930 frinxp 5750 ordelord 6375 foco2 7093 frxp 8094 mpocurryd 8236 omsmolem 8639 erth 8735 unblem1 9278 unwdomg 9561 cflim2 10240 distrlem1pr 11002 uz11 12829 elpq 12941 xmulge0 13245 max0add 15239 lcmfunsnlem2lem1 16557 divgcdcoprm0 16584 cncongr1 16586 prmpwdvds 16819 imasleval 17469 dfgrp3lem 18895 resscntz 19162 ablfac1c 19900 lbsind 20640 isphld 21140 mplcoe5lem 21522 cply1mul 21747 smadiadetr 22106 chfacfisf 22285 chfacfisfcpmat 22286 chcoeffeq 22317 cayhamlem3 22318 tx1stc 23083 ioorcl 25023 coemullem 25693 xrlimcnp 26400 fsumdvdscom 26616 fsumvma 26643 cusgrres 28570 usgredgsscusgredg 28581 clwlkclwwlklem2a 29116 clwwlkext2edg 29174 frgrwopreglem5ALT 29440 frgr2wwlkeu 29445 frgr2wwlk1 29447 grpoidinvlem3 29622 htthlem 30033 atcvat4i 31513 abfmpeld 31748 ressupprn 31783 isarchi3 32204 qsidomlem2 32423 ordtconnlem1 32735 gonarlem 34216 fmlasucdisj 34221 funpartfun 34745 relowlssretop 36048 ltflcei 36280 neificl 36426 keridl 36705 eqvrelth 37286 cvrat4 38119 ps-2 38154 mpaaeu 41663 clcnvlem 42145 fcoresf1 45551 iccpartiltu 45862 2pwp1prm 46029 bgoldbtbnd 46249 lmod0rng 46414 lincext1 46783 |
Copyright terms: Public domain | W3C validator |