Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iba | Structured version Visualization version GIF version |
Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) |
Ref | Expression |
---|---|
iba | ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.21 475 | . 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) | |
2 | simpl 486 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓) | |
3 | 1, 2 | impbid1 228 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ 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: ibar 532 biantru 533 biantrud 535 ancrb 551 pm5.54 1018 dedlem0a 1044 unineq 4189 fvopab6 6848 fressnfv 6972 tpostpos 7985 odi 8304 nnmword 8358 ltmpi 10515 maducoeval2 21534 mdbr2 30374 mdsl2i 30400 poimirlem26 35538 poimirlem27 35539 itg2addnclem 35563 itg2addnclem3 35565 prjspeclsp 40157 rmydioph 40537 expdioph 40546 dmafv2rnb 44391 |
Copyright terms: Public domain | W3C validator |