![]() |
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 514 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: impac 554 equvinva 2034 sbcg 3822 reuan 3856 2reu1 3857 reupick 4282 reusv2lem3 5359 ssrelrn 5854 relssres 5982 funmo 6520 funmoOLD 6521 funssres 6549 dffo4 7057 dffo5 7058 dfwe2 7712 ordpwsuc 7754 ordunisuc2 7784 dfom2 7808 nnsuc 7824 nnaordex 8589 wdom2d 9524 iundom2g 10484 fzospliti 13613 rexuz3 15242 qredeq 16541 prmdvdsfz 16589 dirge 18500 lssssr 20458 lpigen 20771 psgnodpm 21015 neiptopnei 22506 metustexhalf 23935 dyadmbllem 24986 3cyclfrgrrn2 29280 atexch 31372 ordtconnlem1 32569 bj-ideqg1 35685 bj-imdirval3 35705 isbasisrelowllem1 35876 isbasisrelowllem2 35877 pibt2 35938 phpreu 36112 poimirlem26 36154 sstotbnd3 36285 eqlkr3 37613 dihatexv 39851 dvh3dim2 39961 prjspner1 41011 oasubex 41668 naddwordnexlem4 41765 neik0pk1imk0 42411 pm14.123b 42798 ordpss 42823 climreeq 43944 itscnhlc0xyqsol 46941 |
Copyright terms: Public domain | W3C validator |