![]() |
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: a2and 888 mo2v 2614 el 4996 fpropnf1 6688 findcard2d 8369 cantnflem1 8761 ackbij1lem16 9269 fin1a2lem10 9443 inar1 9809 grur1a 9853 sqrt2irr 15198 lcmf 15568 lcmfunsnlem 15576 exprmfct 15638 pockthg 15832 prmgaplem5 15981 prmgaplem6 15982 drsdirfi 17159 obslbs 20296 mdetunilem9 20648 iscnp4 21289 isreg2 21403 dfconn2 21444 1stccnp 21487 flftg 22021 cnpfcf 22066 tsmsxp 22179 nmoleub 22756 vitalilem2 23597 vitalilem5 23600 c1lip1 23979 aalioulem6 24311 jensen 24935 2sqlem6 25368 dchrisumlem3 25400 pntlem3 25518 finsumvtxdg2sstep 26676 bnj849 31323 cvmlift2lem1 31612 cvmlift2lem12 31624 mclsax 31794 nn0prpwlem 32644 bj-el 33124 matunitlindflem1 33736 poimirlem30 33770 mapdordlem2 37446 iccelpart 41897 sbgoldbalt 42197 sbgoldbm 42200 evengpop3 42214 evengpoap3 42215 bgoldbtbnd 42225 lindslinindsimp1 42774 |
Copyright terms: Public domain | W3C validator |