| 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 2486 dfmoeu 2536 disj 4450 elALT2 5369 fpropnf1 7287 findcard2d 9206 cantnflem1 9729 ttrclss 9760 ackbij1lem16 10274 fin1a2lem10 10449 inar1 10815 grur1a 10859 sqrt2irr 16285 lcmf 16670 lcmfunsnlem 16678 exprmfct 16741 pockthg 16944 prmgaplem5 17093 prmgaplem6 17094 drsdirfi 18351 obslbs 21750 mdetunilem9 22626 iscnp4 23271 isreg2 23385 dfconn2 23427 1stccnp 23470 flftg 24004 cnpfcf 24049 tsmsxp 24163 nmoleub 24752 vitalilem2 25644 vitalilem5 25647 c1lip1 26036 aalioulem6 26379 jensen 27032 2sqlem6 27467 dchrisumlem3 27535 pntlem3 27653 finsumvtxdg2sstep 29567 dfufd2lem 33577 bnj849 34939 cvmlift2lem1 35307 cvmlift2lem12 35319 mclsax 35574 nn0prpwlem 36323 matunitlindflem1 37623 poimirlem30 37657 mapdordlem2 41639 eu6w 42686 iccelpart 47420 ichreuopeq 47460 sbgoldbalt 47768 sbgoldbm 47771 evengpop3 47785 evengpoap3 47786 bgoldbtbnd 47796 lindslinindsimp1 48374 iscnrm3r 48845 iscnrm3l 48848 |
| Copyright terms: Public domain | W3C validator |