![]() |
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 527 | 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: imdistani 570 pwpw0 4817 sssn 4830 pwsnOLD 4902 wfisgOLD 6356 ordtr2 6409 tfis 7844 oeordi 8587 unblem3 9297 trcl 9723 frinsg 9746 clwlkclwwlkfo 29293 h1datomi 30865 ballotlemfc0 33522 ballotlemfcc 33523 pthisspthorcycl 34150 dfrdg4 34954 bj-sbsb 35763 bj-opelidres 36090 clsk1indlem3 42842 sbiota1 43241 |
Copyright terms: Public domain | W3C validator |