| 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 4813 sssn 4826 wfisgOLD 6375 ordtr2 6428 tfis 7876 oeordi 8625 unblem3 9330 trcl 9768 frinsg 9791 pthisspthorcycl 29822 clwlkclwwlkfo 30028 h1datomi 31600 ballotlemfc0 34495 ballotlemfcc 34496 dfrdg4 35952 bj-sbsb 36838 bj-opelidres 37162 clsk1indlem3 44056 sbiota1 44453 |
| Copyright terms: Public domain | W3C validator |