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 3312 tfindsg2 7564 tz7.49c 8073 ssenen 8680 pssnn 8725 unwdomg 9037 cff1 9669 cfsmolem 9681 cfpwsdom 9995 wunex2 10149 mulgt0sr 10516 uzwo 12300 shftfval 14419 fsum2dlem 15115 fprod2dlem 15324 prmpwdvds 16230 quscrng 19943 chfacfscmul0 21396 chfacfpmmul0 21400 tgtop 21511 neitr 21718 bwth 21948 tx1stc 22188 cnextcn 22605 logfac2 25721 2sqmo 25941 outpasch 26469 trgcopyeu 26520 axcontlem12 26689 spanuni 29249 pjnmopi 29853 superpos 30059 atcvat4i 30102 rabeqsnd 30192 fpwrelmap 30396 locfinreflem 31004 cmpcref 31014 loop1cycl 32282 fneint 33594 neibastop3 33608 isbasisrelowllem1 34519 isbasisrelowllem2 34520 relowlssretop 34527 finxpreclem6 34560 ralssiun 34571 fin2so 34761 matunitlindflem2 34771 poimirlem26 34800 poimirlem27 34801 heicant 34809 ismblfin 34815 ovoliunnfl 34816 itg2gt0cn 34829 cvrat4 36461 pell14qrexpcl 39344 liminflimsupxrre 41978 odz2prm2pw 43572 prelrrx2b 44599 |
Copyright terms: Public domain | W3C validator |