![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimpar | GIF version |
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
Ref | Expression |
---|---|
biimpa.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
biimpar | ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimpa.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | biimprd 156 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
3 | 2 | imp 122 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: exbiri 374 bitr 456 eqtr 2100 opabss 3862 euotd 4037 wetriext 4347 sosng 4459 xpsspw 4498 brcogw 4552 funimaexglem 5033 funfni 5050 fnco 5058 fnssres 5063 fn0 5069 fnimadisj 5070 fnimaeq0 5071 foco 5167 foimacnv 5195 fvelimab 5281 fvopab3ig 5298 dff3im 5364 dffo4 5367 fmptco 5382 f1eqcocnv 5482 f1ocnv2d 5755 fnexALT 5791 xp1st 5843 xp2nd 5844 tfrlemiubacc 5999 tfri2d 6005 tfr1onlemubacc 6015 tfrcllemubacc 6028 tfri3 6036 ecelqsg 6246 elqsn0m 6261 fidifsnen 6426 recclnq 6696 nq0a0 6761 qreccl 8860 difelfzle 9274 exfzdc 9378 modifeq2int 9520 frec2uzlt2d 9538 1elfz0hash 9882 caucvgrelemcau 10067 recvalap 10184 fzomaxdiflem 10199 divconjdvds 10457 ndvdssub 10537 zsupcllemstep 10548 rplpwr 10623 dvdssqlem 10626 eucialgcvga 10647 mulgcddvds 10683 isprm2lem 10705 |
Copyright terms: Public domain | W3C validator |