|   | 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 207 df-an 396 | 
| This theorem is referenced by: reximd2a 3268 rabeqsnd 4668 tfindsg2 7884 tz7.49c 8487 domssl 9039 domssr 9040 ssenen 9192 pssnn 9209 unfi 9212 unwdomg 9625 cff1 10299 cfsmolem 10311 cfpwsdom 10625 wunex2 10779 mulgt0sr 11146 uzwo 12954 shftfval 15110 fsum2dlem 15807 fprod2dlem 16017 prmpwdvds 16943 ghmqusnsglem2 19300 ghmquskerlem2 19304 quscrng 21294 ring2idlqusb 21321 chfacfscmul0 22865 chfacfpmmul0 22869 tgtop 22981 neitr 23189 bwth 23419 tx1stc 23659 cnextcn 24076 logfac2 27262 2sqmo 27482 outpasch 28764 trgcopyeu 28815 axcontlem12 28991 spanuni 31564 pjnmopi 32168 superpos 32374 atcvat4i 32417 2ndresdju 32660 fpwrelmap 32745 chnind 33002 gsumwun 33069 gsumwrd2dccatlem 33070 wrdpmtrlast 33114 nsgqusf1olem2 33443 ssmxidl 33503 r1plmhm 33631 r1pquslmic 33632 ply1degltdimlem 33674 locfinreflem 33840 cmpcref 33850 loop1cycl 35143 fneint 36350 neibastop3 36364 isbasisrelowllem1 37357 isbasisrelowllem2 37358 relowlssretop 37365 finxpreclem6 37398 ralssiun 37409 fin2so 37615 matunitlindflem2 37625 poimirlem26 37654 poimirlem27 37655 heicant 37663 ismblfin 37669 ovoliunnfl 37670 itg2gt0cn 37683 cvrat4 39446 pell14qrexpcl 42883 cantnfresb 43342 liminflimsupxrre 45837 odz2prm2pw 47555 prelrrx2b 48640 opnneilv 48813 intubeu 48888 unilbeu 48889 | 
| Copyright terms: Public domain | W3C validator |