Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ancri | Structured version Visualization version GIF version |
Description: Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
Ref | Expression |
---|---|
ancri.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ancri | ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancri.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
3 | 1, 2 | jca 554 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 197 df-an 386 |
This theorem is referenced by: bamalip 2586 gencbvex 3250 eusv2nf 4864 issref 5509 trsuc 5810 fo00 6172 eqfnov2 6767 caovmo 6871 bropopvvv 7255 tz7.48lem 7536 tz7.48-1 7538 oewordri 7672 epfrs 8607 ordpipq 9764 ltexprlem4 9861 xrinfmsslem 12138 hashfzp1 13218 swrdccat3a 13494 dfgcd2 15263 catpropd 16369 idmhm 17344 symg2bas 17818 psgndiflemB 19946 pmatcollpw2lem 20582 icccvx 22749 uspgr1v1eop 26141 esumcst 30125 ddemeas 30299 bnj600 30989 bnj852 30991 dfpo2 31645 bj-csbsnlem 32898 bj-ismooredr2 33065 nzss 38516 iotasbc 38620 wallispilem3 40284 nnsum3primes4 41676 idmgmhm 41788 |
Copyright terms: Public domain | W3C validator |