![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ibar | Structured version Visualization version GIF version |
Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) |
Ref | Expression |
---|---|
ibar | ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2 455 | . 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
2 | simpr 471 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
3 | 1, 2 | impbid1 215 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 |
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 383 |
This theorem is referenced by: biantrur 520 biantrurd 522 baib 525 baibd 529 bianabs 531 pm5.42 533 anclb 535 anabs5 642 annotanannot 830 pm5.33 831 pclem6 1011 moanim 2678 euan 2679 eueq3 3533 reu6 3547 ifan 4274 dfopif 4537 reusv2lem5 5003 fvopab3g 6421 riota1a 6775 dfom2 7217 suppssr 7481 mpt2curryd 7550 boxcutc 8108 funisfsupp 8439 dfac3 9147 eluz2 11898 elixx3g 12392 elfz2 12539 zmodid2 12905 shftfib 14019 dvdsssfz1 15248 modremain 15339 sadadd2lem2 15379 smumullem 15421 issubg 17801 resgrpisgrp 17822 sscntz 17965 pgrpsubgsymgbi 18033 issubrg 18989 lindsmm 20383 mdetunilem8 20642 mdetunilem9 20643 cmpsub 21423 txcnmpt 21647 fbfinnfr 21864 elfilss 21899 fixufil 21945 ibladdlem 23805 iblabslem 23813 cusgruvtxb 26552 usgr0edg0rusgr 26705 rgrusgrprc 26719 rusgrnumwwlkslem 27117 eclclwwlkn1 27232 eupth2lem1 27397 pjimai 29374 chrelati 29562 tltnle 30001 metidv 30274 slenlt 32213 curf 33719 unccur 33724 cnambfre 33789 itg2addnclem2 33793 ibladdnclem 33797 iblabsnclem 33804 expdiophlem1 38114 rfovcnvf1od 38824 fsovrfovd 38829 ntrneiel2 38910 reuan 41697 odd2np1ALTV 42110 isrnghm 42417 rnghmval2 42420 uzlidlring 42454 islindeps 42767 elbigo2 42871 |
Copyright terms: Public domain | W3C validator |