| 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 511 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: gencbvex 3541 eusv2nf 5395 dfpo2 6316 trsuc 6471 fo00 6884 eqfnov2 7563 caovmo 7670 bropopvvv 8115 tz7.48lem 8481 tz7.48-1 8483 oewordri 8630 epfrs 9771 ordpipq 10982 ltexprlem4 11079 xrinfmsslem 13350 hashfzp1 14470 dfgcd2 16583 catpropd 17752 idmgmhm 18714 symg2bas 19410 psgndiflemB 21618 pmatcollpw2lem 22783 icccvx 24981 uspgr1v1eop 29266 esumcst 34064 ddemeas 34237 bnj600 34933 bnj852 34935 satfvsucsuc 35370 satffunlem2lem2 35411 satffunlem2 35413 bj-csbsnlem 36904 bj-elid6 37171 aks6d1c6isolem3 42177 nzss 44336 iotasbc 44438 wallispilem3 46082 dfafv2 47144 nnsum3primes4 47775 |
| Copyright terms: Public domain | W3C validator |