![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimp3a | GIF version |
Description: Infer implication from a logical equivalence. Similar to biimpa 290. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
biimp3a.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
biimp3a | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp3a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | biimpa 290 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | 3impa 1134 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 ∧ w3a 920 |
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 df-3an 922 |
This theorem is referenced by: nnawordex 6189 nn0addge1 8471 nn0addge2 8472 nn0sub2 8572 eluzp1p1 8795 uznn0sub 8801 iocssre 9122 icossre 9123 iccssre 9124 lincmb01cmp 9171 iccf1o 9172 fzosplitprm1 9390 subfzo0 9398 modfzo0difsn 9547 fldivndvdslt 10560 hashgcdlem 10828 |
Copyright terms: Public domain | W3C validator |