![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anc2li | Structured version Visualization version GIF version |
Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.) |
Ref | Expression |
---|---|
anc2li.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
anc2li | ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anc2li.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
3 | 1, 2 | jctild 525 | 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: imdistani 568 pwpw0 4818 sssn 4831 wfisgOLD 6377 ordtr2 6430 tfis 7876 oeordi 8624 unblem3 9328 trcl 9766 frinsg 9789 clwlkclwwlkfo 30038 h1datomi 31610 ballotlemfc0 34474 ballotlemfcc 34475 pthisspthorcycl 35113 dfrdg4 35933 bj-sbsb 36820 bj-opelidres 37144 clsk1indlem3 44033 sbiota1 44430 |
Copyright terms: Public domain | W3C validator |