Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > expl | Structured version Visualization version GIF version |
Description: Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.) |
Ref | Expression |
---|---|
expl.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
expl | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expl.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
2 | 1 | exp31 420 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 411 | 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: reximd2a 3309 tfindsg2 7565 tz7.49c 8071 ssenen 8679 pssnn 8724 unwdomg 9036 cff1 9668 cfsmolem 9680 cfpwsdom 9994 wunex2 10148 mulgt0sr 10515 uzwo 12299 shftfval 14417 fsum2dlem 15113 fprod2dlem 15322 prmpwdvds 16228 quscrng 19941 chfacfscmul0 21394 chfacfpmmul0 21398 tgtop 21509 neitr 21716 bwth 21946 tx1stc 22186 cnextcn 22603 logfac2 25720 2sqmo 25940 outpasch 26468 trgcopyeu 26519 axcontlem12 26688 spanuni 29248 pjnmopi 29852 superpos 30058 atcvat4i 30101 rabeqsnd 30191 fpwrelmap 30395 locfinreflem 31003 cmpcref 31013 loop1cycl 32281 fneint 33593 neibastop3 33607 isbasisrelowllem1 34518 isbasisrelowllem2 34519 relowlssretop 34526 finxpreclem6 34559 ralssiun 34570 fin2so 34760 matunitlindflem2 34770 poimirlem26 34799 poimirlem27 34800 heicant 34808 ismblfin 34814 ovoliunnfl 34815 itg2gt0cn 34828 cvrat4 36459 pell14qrexpcl 39342 liminflimsupxrre 41974 odz2prm2pw 43602 prelrrx2b 44629 |
Copyright terms: Public domain | W3C validator |