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 531 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓))) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: ifptru 1075 cad1 1623 raldifeq 4390 rexreusng 4580 posn 5618 elrnmpt1 5811 dfres3 5840 opelres 5841 ffrnbd 6531 fliftf 7094 eroveu 8436 ixpfi2 8908 elfi2 8964 dffi3 8981 cfss 9778 wunex2 10251 nnle1eq1 11759 nn0le0eq0 12017 ixxun 12850 ioopos 12911 injresinj 13262 hashle00 13866 prprrab 13938 xpcogend 14436 cnpart 14702 fz1f1o 15173 nndivdvds 15721 dvdsmultr2 15756 bitsmod 15892 sadadd 15923 sadass 15927 smuval2 15938 smumul 15949 pcmpt 16341 pcmpt2 16342 prmreclem2 16366 prmreclem5 16369 ramcl 16478 mrcidb2 17005 acsfn 17046 fncnvimaeqv 17499 latleeqj1 17802 resmndismnd 18102 pgpssslw 18870 subgdmdprd 19288 acsfn1p 19710 lssle0 19853 islpir2 20156 islinds3 20663 iscld4 21829 cncnpi 22042 cnprest2 22054 lmss 22062 isconn2 22178 dfconn2 22183 subislly 22245 lly1stc 22260 elptr 22337 txcn 22390 xkoinjcn 22451 tsmsres 22908 isxmet2d 23093 xmetgt0 23124 prdsxmetlem 23134 imasdsf1olem 23139 xblss2 23168 stdbdbl 23283 prdsxmslem2 23295 xrtgioo 23571 xrsxmet 23574 cnmpopc 23693 elpi1i 23811 minveclem7 24200 elovolmr 24241 ismbf 24393 mbfmax 24414 itg1val2 24449 mbfi1fseqlem4 24484 itgresr 24544 iblrelem 24556 iblpos 24558 rlimcnp 25716 rlimcnp2 25717 chpchtsum 25968 lgsneg 26070 lgsdilem 26073 2lgslem1a 26140 lmiinv 26751 isspthonpth 27703 s3wwlks2on 27907 clwlkclwwlk 27952 clwwlknonel 28045 clwwlknun 28062 eupth2lem2 28169 frgr3vlem2 28224 numclwwlk2lem1 28326 minvecolem7 28831 shle0 29390 mdsl2bi 30271 dmdbr5ati 30370 cdj3lem1 30382 eulerpartlemr 31924 subfacp1lem3 32728 satefvfmla1 32971 eqscut2 33656 hfext 34141 bj-issetwt 34715 poimirlem25 35458 poimirlem26 35459 poimirlem27 35460 mblfinlem3 35472 mblfinlem4 35473 mbfresfi 35479 itg2addnclem 35484 itg2addnc 35487 heiborlem10 35634 dffunsALTV2 36451 dffunsALTV3 36452 dffunsALTV4 36453 elfunsALTV2 36460 elfunsALTV3 36461 elfunsALTV4 36462 elfunsALTV5 36463 dfdisjs2 36476 dfdisjs5 36479 eldisjs2 36490 ople0 36857 atlle0 36975 cdlemg10c 38309 cdlemg33c 38378 hdmap14lem13 39550 mrefg3 40143 radcnvrat 41511 2ffzoeq 44402 |
Copyright terms: Public domain | W3C validator |