![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > embantd | Structured version Visualization version Unicode 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 54 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpid 42 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: a2and 825 mo2v 2316 el 4598 findcard2d 7838 cantnflem1 8219 ackbij1lem16 8690 fin1a2lem10 8864 inar1 9225 grur1a 9269 sqrt2irr 14349 lcmf 14654 lcmfunsnlem 14662 exprmfct 14696 pockthg 14898 prmgaplem5 15073 prmgaplem6 15074 drsdirfi 16231 obslbs 19341 mdetunilem9 19693 iscnp4 20327 isreg2 20441 dfcon2 20482 1stccnp 20525 flftg 21059 cnpfcf 21104 tsmsxp 21217 nmoleub 21784 nmoleubOLD 21800 vitalilem2 22615 vitalilem5 22618 c1lip1 22997 aalioulem6 23341 jensen 23962 2sqlem6 24345 dchrisumlem3 24377 pntlem3 24495 bnj849 29784 cvmlift2lem1 30073 cvmlift2lem12 30085 mclsax 30255 nn0prpwlem 31026 bj-el 31455 poimirlem30 32014 mapdordlem2 35249 iccelpart 38784 sgoldbalt 38919 evengpop3 38930 evengpoap3 38931 bgoldbtbnd 38941 fpropnf1 39077 lindslinindsimp1 40522 |
Copyright terms: Public domain | W3C validator |