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 2047 barbari 2108 cesaro 2114 camestros 2115 calemos 2125 swopo 4266 elrnrexdm 5606 tfrcl 6311 ixpsnf1o 6681 fidcenumlemrk 6898 subhalfnqq 7334 enq0ref 7353 prarloc 7423 letrp1 8719 p1le 8720 peano2uz2 9271 uzind 9275 uzid 9453 qreccl 9551 fprodsplit1f 11531 |
Copyright terms: Public domain | W3C validator |