Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > embantd | Structured version Visualization version GIF version |
Description: Deduction embedding an antecedent. (Contributed by Wolf Lammen, 4-Oct-2013.) |
Ref | Expression |
---|---|
embantd.1 | ⊢ (𝜑 → 𝜓) |
embantd.2 | ⊢ (𝜑 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
embantd | ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | embantd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | embantd.2 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
3 | 2 | imim2d 57 | . 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃))) |
4 | 1, 3 | mpid 44 | 1 ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: dfsb1 2510 dfmoeu 2618 el 5272 fpropnf1 7027 findcard2d 8762 cantnflem1 9154 ackbij1lem16 9659 fin1a2lem10 9833 inar1 10199 grur1a 10243 sqrt2irr 15604 lcmf 15979 lcmfunsnlem 15987 exprmfct 16050 pockthg 16244 prmgaplem5 16393 prmgaplem6 16394 drsdirfi 17550 obslbs 20876 mdetunilem9 21231 iscnp4 21873 isreg2 21987 dfconn2 22029 1stccnp 22072 flftg 22606 cnpfcf 22651 tsmsxp 22765 nmoleub 23342 vitalilem2 24212 vitalilem5 24215 c1lip1 24596 aalioulem6 24928 jensen 25568 2sqlem6 26001 dchrisumlem3 26069 pntlem3 26187 finsumvtxdg2sstep 27333 bnj849 32199 cvmlift2lem1 32551 cvmlift2lem12 32563 mclsax 32818 nn0prpwlem 33672 matunitlindflem1 34890 poimirlem30 34924 mapdordlem2 38775 iccelpart 43600 ichreuopeq 43642 sbgoldbalt 43953 sbgoldbm 43956 evengpop3 43970 evengpoap3 43971 bgoldbtbnd 43981 lindslinindsimp1 44519 |
Copyright terms: Public domain | W3C validator |