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 528 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓))) | |
3 | 1, 2 | syl 17 | 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: ifptru 1073 cad1 1619 raldifeq 4425 rexreusng 4616 posn 5673 elrnmpt1 5870 dfres3 5899 opelres 5900 ffrnbd 6625 fliftf 7195 eroveu 8610 ixpfi2 9126 elfi2 9182 dffi3 9199 cfss 10030 wunex2 10503 nnle1eq1 12012 nn0le0eq0 12270 ixxun 13104 ioopos 13165 injresinj 13517 hashle00 14124 prprrab 14196 xpcogend 14694 cnpart 14960 fz1f1o 15431 nndivdvds 15981 dvdsmultr2 16016 bitsmod 16152 sadadd 16183 sadass 16187 smuval2 16198 smumul 16209 pcmpt 16602 pcmpt2 16603 prmreclem2 16627 prmreclem5 16630 ramcl 16739 mrcidb2 17336 acsfn 17377 fncnvimaeqv 17845 latleeqj1 18178 resmndismnd 18456 pgpssslw 19228 subgdmdprd 19646 acsfn1p 20076 lssle0 20220 islpir2 20531 islinds3 21050 iscld4 22225 cncnpi 22438 cnprest2 22450 lmss 22458 isconn2 22574 dfconn2 22579 subislly 22641 lly1stc 22656 elptr 22733 txcn 22786 xkoinjcn 22847 tsmsres 23304 isxmet2d 23489 xmetgt0 23520 prdsxmetlem 23530 imasdsf1olem 23535 xblss2 23564 stdbdbl 23682 prdsxmslem2 23694 xrtgioo 23978 xrsxmet 23981 cnmpopc 24100 elpi1i 24218 minveclem7 24608 elovolmr 24649 ismbf 24801 mbfmax 24822 itg1val2 24857 mbfi1fseqlem4 24892 itgresr 24952 iblrelem 24964 iblpos 24966 rlimcnp 26124 rlimcnp2 26125 chpchtsum 26376 lgsneg 26478 lgsdilem 26481 2lgslem1a 26548 lmiinv 27162 isspthonpth 28126 s3wwlks2on 28330 clwlkclwwlk 28375 clwwlknonel 28468 clwwlknun 28485 eupth2lem2 28592 frgr3vlem2 28647 numclwwlk2lem1 28749 minvecolem7 29254 shle0 29813 mdsl2bi 30694 dmdbr5ati 30793 cdj3lem1 30805 eulerpartlemr 32350 subfacp1lem3 33153 satefvfmla1 33396 eqscut2 34009 hfext 34494 bj-issetwt 35068 poimirlem25 35811 poimirlem26 35812 poimirlem27 35813 mblfinlem3 35825 mblfinlem4 35826 mbfresfi 35832 itg2addnclem 35837 itg2addnc 35840 heiborlem10 35987 dffunsALTV2 36802 dffunsALTV3 36803 dffunsALTV4 36804 elfunsALTV2 36811 elfunsALTV3 36812 elfunsALTV4 36813 elfunsALTV5 36814 dfdisjs2 36827 dfdisjs5 36830 eldisjs2 36841 ople0 37208 atlle0 37326 cdlemg10c 38660 cdlemg33c 38729 hdmap14lem13 39901 mrefg3 40537 radcnvrat 41939 2ffzoeq 44831 |
Copyright terms: Public domain | W3C validator |