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 564 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: imdistani 722 pwpw0 4284 sssn 4298 pwsnALT 4367 wfisg 5632 ordtr2 5685 tfis 6946 oeordi 7554 unblem3 8099 trcl 8487 h1datomi 27824 ballotlemfc0 29881 ballotlemfcc 29882 frinsg 30986 dfrdg4 31228 bj-sbsb 32012 clsk1indlem3 37361 sbiota1 37657 |
Copyright terms: Public domain | W3C validator |