![]() |
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 419 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 410 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 396 |
This theorem is referenced by: reximd2a 3258 rabeqsnd 4663 tfindsg2 7844 tz7.49c 8441 domssl 8989 domssr 8990 ssenen 9146 pssnn 9163 unfi 9167 pssnnOLD 9260 unwdomg 9574 cff1 10248 cfsmolem 10260 cfpwsdom 10574 wunex2 10728 mulgt0sr 11095 uzwo 12891 shftfval 15013 fsum2dlem 15712 fprod2dlem 15920 prmpwdvds 16833 quscrng 21123 ring2idlqusb 21148 chfacfscmul0 22670 chfacfpmmul0 22674 tgtop 22786 neitr 22994 bwth 23224 tx1stc 23464 cnextcn 23881 logfac2 27054 2sqmo 27274 outpasch 28430 trgcopyeu 28481 axcontlem12 28657 spanuni 31221 pjnmopi 31825 superpos 32031 atcvat4i 32074 2ndresdju 32298 fpwrelmap 32382 nsgqusf1olem2 32956 ghmquskerlem2 32961 ssmxidl 33021 r1plmhm 33112 r1pquslmic 33113 ply1degltdimlem 33152 locfinreflem 33275 cmpcref 33285 loop1cycl 34583 fneint 35689 neibastop3 35703 isbasisrelowllem1 36692 isbasisrelowllem2 36693 relowlssretop 36700 finxpreclem6 36733 ralssiun 36744 fin2so 36931 matunitlindflem2 36941 poimirlem26 36970 poimirlem27 36971 heicant 36979 ismblfin 36985 ovoliunnfl 36986 itg2gt0cn 36999 cvrat4 38770 pell14qrexpcl 42060 cantnfresb 42529 liminflimsupxrre 44984 odz2prm2pw 46682 prelrrx2b 47554 opnneilv 47695 intubeu 47763 unilbeu 47764 |
Copyright terms: Public domain | W3C validator |