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 2038 barbari 2099 cesaro 2105 camestros 2106 calemos 2116 swopo 4223 elrnrexdm 5552 tfrcl 6254 ixpsnf1o 6623 fidcenumlemrk 6835 subhalfnqq 7215 enq0ref 7234 prarloc 7304 letrp1 8599 p1le 8600 peano2uz2 9151 uzind 9155 uzid 9333 qreccl 9427 |
Copyright terms: Public domain | W3C validator |