![]() |
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 208 df-an 397 |
This theorem is referenced by: sbc2iedv 3779 csbie2t 3846 frinxp 5520 ordelord 6088 foco2 6736 frxp 7673 mpocurryd 7786 omsmolem 8130 erth 8188 unblem1 8616 unwdomg 8894 cflim2 9531 distrlem1pr 10293 uz11 12116 elpq 12224 xmulge0 12527 max0add 14504 lcmfunsnlem2lem1 15811 divgcdcoprm0 15838 cncongr1 15840 prmpwdvds 16069 imasleval 16643 dfgrp3lem 17954 resscntz 18203 ablfac1c 18910 lbsind 19542 mplcoe5lem 19935 cply1mul 20145 isphld 20480 smadiadetr 20968 chfacfisf 21146 chfacfisfcpmat 21147 chcoeffeq 21178 cayhamlem3 21179 tx1stc 21942 ioorcl 23861 coemullem 24523 xrlimcnp 25228 fsumdvdscom 25444 fsumvma 25471 cusgrres 26913 usgredgsscusgredg 26924 clwlkclwwlklem2a 27463 clwwlkext2edg 27522 frgrwopreglem5ALT 27793 frgr2wwlkeu 27798 frgr2wwlk1 27800 grpoidinvlem3 27974 htthlem 28385 atcvat4i 29865 abfmpeld 30089 isarchi3 30454 ordtconnlem1 30784 gonarlem 32249 fmlasucdisj 32254 funpartfun 33013 relowlssretop 34175 ltflcei 34411 neificl 34560 keridl 34842 eqvrelth 35377 cvrat4 36110 ps-2 36145 mpaaeu 39235 clcnvlem 39468 iccpartiltu 43064 2pwp1prm 43233 bgoldbtbnd 43456 lmod0rng 43617 lincext1 43989 |
Copyright terms: Public domain | W3C validator |