![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ancrd | Structured version Visualization version Unicode version |
Description: Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
Ref | Expression |
---|---|
ancrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ancrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancrd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | idd 25 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | jcad 540 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 190 df-an 377 |
This theorem is referenced by: impac 631 equviniv 1883 reupick 3739 prel12 4165 reusv2lem3 4623 ssrnres 5297 funmo 5621 funssres 5645 dffo4 6066 dffo5 6067 dfwe2 6640 ordpwsuc 6674 ordunisuc2 6703 dfom2 6726 nnsuc 6741 nnaordex 7370 wdom2d 8126 iundom2g 8996 fzospliti 11987 rexuz3 13466 prmdvdsfz 14704 qredeq 14718 dirge 16538 lssssr 18231 lpigen 18535 psgnodpm 19211 neiptopnei 20203 metustexhalf 21626 dyadmbllem 22613 3cyclfrgrarn2 25798 atexch 28090 ordtconlem1 28781 isbasisrelowllem1 31804 isbasisrelowllem2 31805 phpreu 31975 poimirlem26 32012 sstotbnd3 32154 eqlkr3 32713 dihatexv 34952 dvh3dim2 35062 pm14.123b 36822 ordpss 36849 climreeq 37779 reuan 38736 2reu1 38742 ssrelrn 39148 |
Copyright terms: Public domain | W3C validator |