![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biantrud | Structured version Visualization version GIF version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.) |
Ref | Expression |
---|---|
biantrud.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
biantrud | ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrud.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | iba 525 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓))) | |
3 | 1, 2 | syl 17 | 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: ifptru 1061 cad1 1704 raldifeq 4203 posn 5344 elrnmpt1 5529 dfres3 5556 fliftf 6729 eroveu 8011 ixpfi2 8431 funsnfsupp 8466 elfi2 8487 dffi3 8504 cfss 9299 wunex2 9772 nn2ge 11257 nnle1eq1 11260 nn0le0eq0 11533 ixxun 12404 ioopos 12463 injresinj 12803 hashle00 13400 prprrab 13467 xpcogend 13934 cnpart 14199 fz1f1o 14660 nndivdvds 15211 dvdsmultr2 15243 bitsmod 15380 sadadd 15411 sadass 15415 smuval2 15426 smumul 15437 pcmpt 15818 pcmpt2 15819 prmreclem2 15843 prmreclem5 15846 ramcl 15955 mrcidb2 16500 acsfn 16541 fncnvimaeqv 16981 latleeqj1 17284 pgpssslw 18249 subgdmdprd 18653 lssle0 19172 islpir2 19473 islinds3 20395 iscld4 21091 discld 21115 cncnpi 21304 cnprest2 21316 lmss 21324 isconn2 21439 dfconn2 21444 subislly 21506 lly1stc 21521 elptr 21598 txcn 21651 hauseqlcld 21671 xkoinjcn 21712 tsmsres 22168 isxmet2d 22353 xmetgt0 22384 prdsxmetlem 22394 imasdsf1olem 22399 xblss2 22428 stdbdbl 22543 prdsxmslem2 22555 xrtgioo 22830 xrsxmet 22833 cncffvrn 22922 cnmpt2pc 22948 elpi1i 23066 minveclem7 23426 elovolmr 23464 ismbf 23616 mbfmax 23635 itg1val2 23670 mbfi1fseqlem4 23704 itgresr 23764 iblrelem 23776 iblpos 23778 itgfsum 23812 rlimcnp 24912 rlimcnp2 24913 chpchtsum 25164 dchreq 25203 lgsneg 25266 lgsdilem 25269 lgsquadlem2 25326 2lgslem1a 25336 lmiinv 25904 isspthonpth 26876 s3wwlks2on 27098 clwlkclwwlk 27146 clwwlknonel 27263 clwwlknun 27282 clwwlknunOLD 27286 dfconngr1 27361 eupth2lem2 27392 frgr3vlem2 27449 numclwwlk2lem1 27558 numclwwlk2lem1OLD 27565 minvecolem7 28069 shle0 28631 mdsl2bi 29512 dmdbr5ati 29611 cdj3lem1 29623 eulerpartlemr 30766 subfacp1lem3 31492 hfext 32617 bj-issetwt 33181 poimirlem25 33765 poimirlem26 33766 poimirlem27 33767 mblfinlem3 33779 mblfinlem4 33780 mbfresfi 33787 itg2addnclem 33792 itg2addnc 33795 cover2 33839 heiborlem10 33950 opelresALTV 34373 ople0 34995 atlle0 35113 cdlemg10c 36447 cdlemg33c 36516 hdmap14lem13 37692 mrefg3 37791 acsfn1p 38289 radcnvrat 39033 funressnfv 41732 dfdfat2 41735 2ffzoeq 41866 |
Copyright terms: Public domain | W3C validator |