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 628 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 446 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: reximd2a 2996 tfindsg2 6953 tz7.49c 7428 ssenen 8019 pssnn 8063 unwdomg 8372 cff1 8963 cfsmolem 8975 cfpwsdom 9285 wunex2 9439 mulgt0sr 9805 uzwo 11627 shftfval 13658 fsum2dlem 14343 fprod2dlem 14549 prmpwdvds 15446 quscrng 19061 chfacfscmul0 20482 chfacfpmmul0 20486 tgtop 20588 neitr 20794 bwth 21023 tx1stc 21263 cnextcn 21681 logfac2 24742 axcontlem12 25655 numclwwlkun 26606 spanuni 27787 pjnmopi 28391 superpos 28597 atcvat4i 28640 fpwrelmap 28896 2sqmo 28980 locfinreflem 29235 cmpcref 29245 fneint 31513 neibastop3 31527 isbasisrelowllem1 32379 isbasisrelowllem2 32380 relowlssretop 32387 finxpreclem6 32409 fin2so 32566 matunitlindflem2 32576 poimirlem26 32605 poimirlem27 32606 heicant 32614 ismblfin 32620 ovoliunnfl 32621 itg2gt0cn 32635 cvrat4 33747 pell14qrexpcl 36449 odz2prm2pw 40013 |
Copyright terms: Public domain | W3C validator |