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 455 eqtr 2098 opabss 3842 euotd 4009 wetriext 4319 sosng 4431 xpsspw 4468 brcogw 4522 funimaexglem 5002 funfni 5019 fnco 5027 fnssres 5032 fn0 5038 fnimadisj 5039 fnimaeq0 5040 foco 5136 foimacnv 5164 fvelimab 5250 fvopab3ig 5267 dff3im 5333 dffo4 5336 fmptco 5351 f1eqcocnv 5451 f1ocnv2d 5724 fnexALT 5760 xp1st 5812 xp2nd 5813 tfrlemiubacc 5967 tfri2d 5973 tfri3 5976 ecelqsg 6182 elqsn0m 6197 fidifsnen 6355 recclnq 6582 nq0a0 6647 qreccl 8727 difelfzle 9145 exfzdc 9249 modifeq2int 9388 frec2uzlt2d 9406 caucvgrelemcau 9866 recvalap 9983 fzomaxdiflem 9998 divconjdvds 10249 ndvdssub 10330 zsupcllemstep 10341 rplpwr 10416 dvdssqlem 10419 eucialgcvga 10440 mulgcddvds 10476 isprm2lem 10498 |
Copyright terms: Public domain | W3C validator |