![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ancrd | Structured version Visualization version GIF 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 24 | . 2 ⊢ (𝜑 → (𝜓 → 𝜓)) | |
3 | 1, 2 | jcad 554 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: impac 650 equviniva 2004 reupick 3944 prel12 4414 reusv2lem3 4901 ssrelrn 5347 ssrnres 5607 funmo 5942 funssres 5968 dffo4 6415 dffo5 6416 dfwe2 7023 ordpwsuc 7057 ordunisuc2 7086 dfom2 7109 nnsuc 7124 nnaordex 7763 wdom2d 8526 iundom2g 9400 fzospliti 12539 rexuz3 14132 qredeq 15418 prmdvdsfz 15464 dirge 17284 lssssr 19001 lpigen 19304 psgnodpm 19982 neiptopnei 20984 metustexhalf 22408 dyadmbllem 23413 3cyclfrgrrn2 27267 atexch 29368 ordtconnlem1 30098 isbasisrelowllem1 33333 isbasisrelowllem2 33334 phpreu 33523 poimirlem26 33565 sstotbnd3 33705 eqlkr3 34706 dihatexv 36944 dvh3dim2 37054 neik0pk1imk0 38662 pm14.123b 38944 ordpss 38972 climreeq 40163 reuan 41501 2reu1 41507 |
Copyright terms: Public domain | W3C validator |