Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biantrud | 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 298 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓))) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpbiran2d 438 posng 4606 elrnmpt1 4785 fliftf 5693 elxp7 6061 eroveu 6513 sbthlemi5 6842 sbthlemi6 6843 elfi2 6853 reapltxor 8344 divap0b 8436 nnle1eq1 8737 nn0le0eq0 8998 nn0lt10b 9124 ioopos 9726 xrmaxiflemcom 11011 fz1f1o 11137 nndivdvds 11488 dvdsmultr2 11522 discld 12294 cncnpi 12386 cnptoprest2 12398 lmss 12404 txcn 12433 isxmet2d 12506 xblss2 12563 bdxmet 12659 xmetxp 12665 cncffvrn 12727 |
Copyright terms: Public domain | W3C validator |