![]() |
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 463 | . 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) | |
2 | simpl 472 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓) | |
3 | 1, 2 | impbid1 215 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ 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: biantru 525 biantrud 527 ancrb 572 pm5.54 963 rbaibr 966 rbaibd 969 dedlem0a 1012 unineq 3910 fvopab6 6350 fressnfv 6467 tpostpos 7417 odi 7704 nnmword 7758 ltmpi 9764 maducoeval2 20494 hausdiag 21496 mdbr2 29283 mdsl2i 29309 poimirlem26 33565 poimirlem27 33566 itg2addnclem 33591 itg2addnclem3 33593 rmydioph 37898 expdioph 37907 |
Copyright terms: Public domain | W3C validator |