![]() |
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 555 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 385 |
This theorem is referenced by: bamalip 2724 gencbvex 3390 eusv2nf 5013 issref 5667 trsuc 5971 fo00 6334 eqfnov2 6933 caovmo 7037 bropopvvv 7424 tz7.48lem 7706 tz7.48-1 7708 oewordri 7843 epfrs 8782 ordpipq 9976 ltexprlem4 10073 xrinfmsslem 12351 hashfzp1 13430 swrdccat3a 13714 dfgcd2 15485 catpropd 16590 idmhm 17565 symg2bas 18038 psgndiflemB 20168 pmatcollpw2lem 20804 icccvx 22970 uspgr1v1eop 26361 esumcst 30455 ddemeas 30629 bnj600 31317 bnj852 31319 dfpo2 31973 bj-csbsnlem 33220 bj-ismooredr2 33389 nzss 39036 iotasbc 39140 wallispilem3 40805 nnsum3primes4 42204 idmgmhm 42316 |
Copyright terms: Public domain | W3C validator |