![]() |
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 147 | . 2 ⊢ (φ → (χ → ψ)) |
3 | 2 | imp 115 | 1 ⊢ ((φ ∧ χ) → ψ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: exbiri 364 bitr 441 eqtr 2054 opabss 3812 euotd 3982 sosng 4356 xpsspw 4393 brcogw 4447 funimaexglem 4925 funfni 4942 fnco 4950 fnssres 4955 fn0 4961 fnimadisj 4962 fnimaeq0 4963 foco 5059 foimacnv 5087 fvelimab 5172 fvopab3ig 5189 dff3im 5255 dffo4 5258 fmptco 5273 f1eqcocnv 5374 f1ocnv2d 5646 fnexALT 5682 xp1st 5734 xp2nd 5735 tfrlemiubacc 5885 tfri2d 5891 tfri3 5894 ecelqsg 6095 elqsn0m 6110 recclnq 6376 nq0a0 6440 qreccl 8351 difelfzle 8762 frec2uzlt2d 8871 |
Copyright terms: Public domain | W3C validator |