![]() |
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 556 | 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 652 equviniva 2101 reupick 4042 prel12OLD 4515 reusv2lem3 5008 ssrelrn 5458 ssrnres 5718 funmo 6053 funssres 6079 dffo4 6526 dffo5 6527 dfwe2 7134 ordpwsuc 7168 ordunisuc2 7197 dfom2 7220 nnsuc 7235 nnaordex 7875 wdom2d 8638 iundom2g 9525 fzospliti 12665 rexuz3 14258 qredeq 15544 prmdvdsfz 15590 dirge 17409 lssssr 19126 lpigen 19429 psgnodpm 20107 neiptopnei 21109 metustexhalf 22533 dyadmbllem 23538 3cyclfrgrrn2 27412 atexch 29520 ordtconnlem1 30250 isbasisrelowllem1 33485 isbasisrelowllem2 33486 phpreu 33675 poimirlem26 33717 sstotbnd3 33857 eqlkr3 34860 dihatexv 37098 dvh3dim2 37208 neik0pk1imk0 38816 pm14.123b 39098 ordpss 39126 climreeq 40317 reuan 41655 2reu1 41661 |
Copyright terms: Public domain | W3C validator |