| 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 527 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓))) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: ifptru 1075 cad1 1617 raldifeq 4494 rexreusng 4679 posn 5771 dmxp 5939 elrnmpt1 5971 dfres3 6002 opelres 6003 ffrnbd 6751 fliftf 7335 eroveu 8852 ixpfi2 9390 elfi2 9454 dffi3 9471 cfss 10305 wunex2 10778 nnle1eq1 12296 nn0le0eq0 12554 ixxun 13403 ioopos 13464 injresinj 13827 hashle00 14439 prprrab 14512 xpcogend 15013 cnpart 15279 fz1f1o 15746 nndivdvds 16299 dvdsmultr2 16335 bitsmod 16473 sadadd 16504 sadass 16508 smuval2 16519 smumul 16530 pcmpt 16930 pcmpt2 16931 prmreclem2 16955 prmreclem5 16958 ramcl 17067 mrcidb2 17661 acsfn 17702 fncnvimaeqv 18164 latleeqj1 18496 resmndismnd 18821 pgpssslw 19632 subgdmdprd 20054 resrhm2b 20602 acsfn1p 20800 lssle0 20948 islpir2 21340 islinds3 21854 iscld4 23073 cncnpi 23286 cnprest2 23298 lmss 23306 isconn2 23422 dfconn2 23427 subislly 23489 lly1stc 23504 elptr 23581 txcn 23634 xkoinjcn 23695 tsmsres 24152 isxmet2d 24337 xmetgt0 24368 prdsxmetlem 24378 imasdsf1olem 24383 xblss2 24412 stdbdbl 24530 prdsxmslem2 24542 xrtgioo 24828 xrsxmet 24831 cnmpopc 24955 elpi1i 25079 minveclem7 25469 elovolmr 25511 ismbf 25663 mbfmax 25684 itg1val2 25719 mbfi1fseqlem4 25753 itgresr 25814 iblrelem 25826 iblpos 25828 rlimcnp 27008 rlimcnp2 27009 chpchtsum 27263 lgsneg 27365 lgsdilem 27368 2lgslem1a 27435 eqscut2 27851 n0subs 28360 lmiinv 28800 isspthonpth 29769 s3wwlks2on 29976 clwlkclwwlk 30021 clwwlknonel 30114 clwwlknun 30131 eupth2lem2 30238 frgr3vlem2 30293 numclwwlk2lem1 30395 nrt2irr 30492 minvecolem7 30902 shle0 31461 mdsl2bi 32342 dmdbr5ati 32441 cdj3lem1 32453 qsfld 33526 eulerpartlemr 34376 subfacp1lem3 35187 satefvfmla1 35430 hfext 36184 bj-issetwt 36876 poimirlem25 37652 poimirlem26 37653 poimirlem27 37654 mblfinlem3 37666 mblfinlem4 37667 mbfresfi 37673 itg2addnclem 37678 itg2addnc 37681 heiborlem10 37827 relssinxpdmrn 38350 dffunsALTV2 38685 dffunsALTV3 38686 dffunsALTV4 38687 elfunsALTV2 38694 elfunsALTV3 38695 elfunsALTV4 38696 elfunsALTV5 38697 dfdisjs2 38710 dfdisjs5 38713 eldisjs2 38724 ople0 39188 atlle0 39306 cdlemg10c 40641 cdlemg33c 40710 hdmap14lem13 41882 mrefg3 42719 onsupneqmaxlim0 43236 onsupnmax 43240 radcnvrat 44333 2ffzoeq 47339 |
| Copyright terms: Public domain | W3C validator |