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 304 | 1 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: pm4.45im 332 mo23 2060 barbari 2121 cesaro 2127 camestros 2128 calemos 2138 swopo 4291 elrnrexdm 5635 tfrcl 6343 ixpsnf1o 6714 fidcenumlemrk 6931 subhalfnqq 7376 enq0ref 7395 prarloc 7465 letrp1 8764 p1le 8765 peano2uz2 9319 uzind 9323 uzid 9501 qreccl 9601 fprodsplit1f 11597 |
Copyright terms: Public domain | W3C validator |