![]() |
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 | iba 528 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | |
2 | 1 | biancomd 464 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 397 |
This theorem is referenced by: biantrurd 533 baib 536 baibd 540 bianabs 542 pm5.42 544 anclb 546 anabs5 661 annotanannot 833 pm5.33 834 pclem6 1024 moanimv 2619 moanim 2620 euan 2621 euanv 2624 ralanid 3098 rexanid 3099 r19.29 3117 rmoanid 3363 reuanid 3364 eueq3 3669 reu6 3684 reuan 3852 ifan 4539 dfopif 4827 notzfaus 5318 reusv2lem5 5357 dmopab2rex 5873 elpredg 6267 fvopab3g 6943 riota1a 7336 dfom2 7804 suppssr 8127 mpocurryd 8200 boxcutc 8879 funisfsupp 9310 dfac3 10057 eluz2 12769 elixx3g 13277 elfz2 13431 zmodid2 13804 shftfib 14957 dvdsssfz1 16200 modremain 16290 sadadd2lem2 16330 smumullem 16372 tltnle 18311 issubg 18928 resgrpisgrp 18949 sscntz 19106 pgrpsubgsymgbi 19190 issubrg 20222 lindsmm 21234 mdetunilem8 21968 mdetunilem9 21969 cmpsub 22751 txcnmpt 22975 hausdiag 22996 fbfinnfr 23192 elfilss 23227 fixufil 23273 ibladdlem 25184 iblabslem 25192 slenlt 27100 cusgruvtxb 28370 usgr0edg0rusgr 28523 rgrusgrprc 28537 rusgrnumwwlkslem 28914 eclclwwlkn1 29019 eupth2lem1 29162 pjimai 31118 chrelati 31306 metidv 32473 satfv1lem 33956 dmopab3rexdif 33999 copsex2b 35611 curf 36056 unccur 36061 cnambfre 36126 itg2addnclem2 36130 ibladdnclem 36134 iblabsnclem 36141 prjsprellsp 40935 expdiophlem1 41331 rfovcnvf1od 42266 fsovrfovd 42271 ntrneiel2 42348 odd2np1ALTV 45856 isrnghm 46180 rnghmval2 46183 uzlidlring 46217 islindeps 46524 elbigo2 46628 |
Copyright terms: Public domain | W3C validator |