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 513 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: impac 553 equvinva 2028 reuan 3877 2reu1 3878 reupick 4284 reusv2lem3 5291 ssrelrn 5756 relssres 5886 funmo 6364 funssres 6391 dffo4 6861 dffo5 6862 dfwe2 7485 ordpwsuc 7519 ordunisuc2 7548 dfom2 7571 nnsuc 7586 nnaordex 8253 wdom2d 9032 iundom2g 9950 fzospliti 13057 rexuz3 14696 qredeq 15989 prmdvdsfz 16037 dirge 17835 lssssr 19654 lpigen 19957 psgnodpm 20660 neiptopnei 21668 metustexhalf 23093 dyadmbllem 24127 3cyclfrgrrn2 27993 atexch 30085 ordtconnlem1 31066 bj-ideqg1 34348 bj-imdirval3 34366 bj-imdirid 34367 isbasisrelowllem1 34518 isbasisrelowllem2 34519 pibt2 34580 phpreu 34757 poimirlem26 34799 sstotbnd3 34935 eqlkr3 36117 dihatexv 38354 dvh3dim2 38464 neik0pk1imk0 40275 pm14.123b 40635 ordpss 40660 climreeq 41770 itscnhlc0xyqsol 44680 |
Copyright terms: Public domain | W3C validator |