| 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 512 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: impac 552 equvinva 2029 sbcg 3863 reuan 3896 2reu1 3897 reupick 4329 reusv2lem3 5400 axprlem4 5426 ssrelrn 5905 relssres 6040 funmo 6581 funmoOLD 6582 funssres 6610 dffo4 7123 dffo5 7124 dfwe2 7794 ordpwsuc 7835 ordunisuc2 7865 dfom2 7889 nnsuc 7905 nnaordex 8676 wdom2d 9620 iundom2g 10580 fzospliti 13731 rexuz3 15387 qredeq 16694 prmdvdsfz 16742 dirge 18648 lssssr 20952 lpigen 21345 psgnodpm 21606 psdmul 22170 neiptopnei 23140 metustexhalf 24569 dyadmbllem 25634 3cyclfrgrrn2 30306 atexch 32400 ordtconnlem1 33923 bj-ideqg1 37165 bj-imdirval3 37185 isbasisrelowllem1 37356 isbasisrelowllem2 37357 pibt2 37418 phpreu 37611 poimirlem26 37653 sstotbnd3 37783 eqlkr3 39102 dihatexv 41340 dvh3dim2 41450 unitscyglem4 42199 prjspner1 42636 oasubex 43299 naddwordnexlem4 43414 neik0pk1imk0 44060 pm14.123b 44445 ordpss 44470 climreeq 45628 uspgrlimlem1 47955 itscnhlc0xyqsol 48686 |
| Copyright terms: Public domain | W3C validator |