Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ancli | GIF version |
Description: Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.) |
Ref | Expression |
---|---|
ancli.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ancli | ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (𝜑 → 𝜑) | |
2 | ancli.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | jca 290 | 1 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 |
This theorem is referenced by: pm4.45im 317 mo23 1941 barbari 2002 cesaro 2008 camestros 2009 calemos 2019 swopo 4043 elrnrexdm 5306 subhalfnqq 6512 enq0ref 6531 prarloc 6601 letrp1 7814 p1le 7815 peano2uz2 8345 uzind 8349 uzid 8487 qreccl 8576 |
Copyright terms: Public domain | W3C validator |