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 472 | . 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) | |
2 | simpl 483 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓) | |
3 | 1, 2 | impbid1 226 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: ibar 529 biantru 530 biantrud 532 ancrb 548 pm5.54 1011 dedlem0a 1035 unineq 4253 fvopab6 6794 fressnfv 6915 tpostpos 7903 odi 8195 nnmword 8249 ltmpi 10315 maducoeval2 21179 mdbr2 30001 mdsl2i 30027 poimirlem26 34800 poimirlem27 34801 itg2addnclem 34825 itg2addnclem3 34827 prjspeclsp 39142 rmydioph 39491 expdioph 39500 dmafv2rnb 43309 |
Copyright terms: Public domain | W3C validator |