![]() |
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 2480 dfmoeu 2530 disj 4446 elALT2 5366 fpropnf1 7262 findcard2d 9162 cantnflem1 9680 ttrclss 9711 ackbij1lem16 10226 fin1a2lem10 10400 inar1 10766 grur1a 10810 sqrt2irr 16188 lcmf 16566 lcmfunsnlem 16574 exprmfct 16637 pockthg 16835 prmgaplem5 16984 prmgaplem6 16985 drsdirfi 18254 obslbs 21276 mdetunilem9 22113 iscnp4 22758 isreg2 22872 dfconn2 22914 1stccnp 22957 flftg 23491 cnpfcf 23536 tsmsxp 23650 nmoleub 24239 vitalilem2 25117 vitalilem5 25120 c1lip1 25505 aalioulem6 25841 jensen 26482 2sqlem6 26915 dchrisumlem3 26983 pntlem3 27101 finsumvtxdg2sstep 28795 bnj849 33924 cvmlift2lem1 34281 cvmlift2lem12 34293 mclsax 34548 nn0prpwlem 35195 matunitlindflem1 36472 poimirlem30 36506 mapdordlem2 40496 iccelpart 46087 ichreuopeq 46127 sbgoldbalt 46435 sbgoldbm 46438 evengpop3 46452 evengpoap3 46453 bgoldbtbnd 46463 lindslinindsimp1 47091 iscnrm3r 47534 iscnrm3l 47537 |
Copyright terms: Public domain | W3C validator |