![]() |
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 296 | . 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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpbiran2d 436 posng 4571 elrnmpt1 4750 fliftf 5654 elxp7 6022 eroveu 6474 sbthlemi5 6801 sbthlemi6 6802 elfi2 6812 reapltxor 8269 divap0b 8356 nnle1eq1 8654 nn0le0eq0 8909 nn0lt10b 9035 ioopos 9626 xrmaxiflemcom 10910 fz1f1o 11036 nndivdvds 11347 dvdsmultr2 11381 discld 12148 cncnpi 12239 cnptoprest2 12251 lmss 12257 txcn 12286 isxmet2d 12337 xblss2 12394 bdxmet 12490 xmetxp 12496 cncffvrn 12555 |
Copyright terms: Public domain | W3C validator |