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 515 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: gencbvex 3469 eusv2nf 5293 trsuc 6302 fo00 6701 eqfnov2 7345 caovmo 7450 bropopvvv 7863 tz7.48lem 8182 tz7.48-1 8184 oewordri 8325 epfrs 9352 ordpipq 10561 ltexprlem4 10658 xrinfmsslem 12903 hashfzp1 14003 dfgcd2 16111 catpropd 17217 symg2bas 18790 psgndiflemB 20567 pmatcollpw2lem 21679 icccvx 23852 uspgr1v1eop 27342 esumcst 31748 ddemeas 31921 bnj600 32617 bnj852 32619 satfvsucsuc 33045 satffunlem2lem2 33086 satffunlem2 33088 dfpo2 33446 bj-csbsnlem 34830 bj-elid6 35081 nzss 41616 iotasbc 41718 wallispilem3 43291 dfafv2 44304 nnsum3primes4 44921 idmgmhm 45023 |
Copyright terms: Public domain | W3C validator |