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 207 ∧ 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 208 df-an 397 |
This theorem is referenced by: ifptru 1065 cad1 1608 raldifeq 4437 rexreusng 4611 posn 5631 elrnmpt1 5824 dfres3 5852 opelres 5853 fliftf 7057 eroveu 8382 ixpfi2 8811 elfi2 8867 dffi3 8884 cfss 9676 wunex2 10149 nnle1eq1 11656 nn0le0eq0 11914 ixxun 12744 ioopos 12803 injresinj 13148 hashle00 13751 prprrab 13821 xpcogend 14324 cnpart 14589 fz1f1o 15057 nndivdvds 15606 dvdsmultr2 15639 bitsmod 15775 sadadd 15806 sadass 15810 smuval2 15821 smumul 15832 pcmpt 16218 pcmpt2 16219 prmreclem2 16243 prmreclem5 16246 ramcl 16355 mrcidb2 16879 acsfn 16920 fncnvimaeqv 17360 latleeqj1 17663 resmndismnd 17963 pgpssslw 18670 subgdmdprd 19087 acsfn1p 19509 lssle0 19652 islpir2 19954 islinds3 20908 iscld4 21603 cncnpi 21816 cnprest2 21828 lmss 21836 isconn2 21952 dfconn2 21957 subislly 22019 lly1stc 22034 elptr 22111 txcn 22164 xkoinjcn 22225 tsmsres 22681 isxmet2d 22866 xmetgt0 22897 prdsxmetlem 22907 imasdsf1olem 22912 xblss2 22941 stdbdbl 23056 prdsxmslem2 23068 xrtgioo 23343 xrsxmet 23346 cnmpopc 23461 elpi1i 23579 minveclem7 23967 elovolmr 24006 ismbf 24158 mbfmax 24179 itg1val2 24214 mbfi1fseqlem4 24248 itgresr 24308 iblrelem 24320 iblpos 24322 rlimcnp 25471 rlimcnp2 25472 chpchtsum 25723 lgsneg 25825 lgsdilem 25828 2lgslem1a 25895 lmiinv 26506 isspthonpth 27458 s3wwlks2on 27663 clwlkclwwlk 27708 clwwlknonel 27802 clwwlknun 27819 eupth2lem2 27926 frgr3vlem2 27981 numclwwlk2lem1 28083 minvecolem7 28588 shle0 29147 mdsl2bi 30028 dmdbr5ati 30127 cdj3lem1 30139 eulerpartlemr 31532 subfacp1lem3 32327 satefvfmla1 32570 hfext 33542 bj-issetwt 34087 poimirlem25 34799 poimirlem26 34800 poimirlem27 34801 mblfinlem3 34813 mblfinlem4 34814 mbfresfi 34820 itg2addnclem 34825 itg2addnc 34828 heiborlem10 34981 dffunsALTV2 35799 dffunsALTV3 35800 dffunsALTV4 35801 elfunsALTV2 35808 elfunsALTV3 35809 elfunsALTV4 35810 elfunsALTV5 35811 dfdisjs2 35824 dfdisjs5 35827 eldisjs2 35838 ople0 36205 atlle0 36323 cdlemg10c 37657 cdlemg33c 37726 hdmap14lem13 38898 mrefg3 39185 radcnvrat 40526 2ffzoeq 43409 |
Copyright terms: Public domain | W3C validator |