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 294. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
biimp3a.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
biimp3a | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp3a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | biimpa 294 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | 3impa 1176 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: nnawordex 6424 div2subap 8596 nn0addge1 9023 nn0addge2 9024 nn0sub2 9124 eluzp1p1 9351 uznn0sub 9357 iocssre 9736 icossre 9737 iccssre 9738 lincmb01cmp 9786 iccf1o 9787 fzosplitprm1 10011 subfzo0 10019 modfzo0difsn 10168 efltim 11404 fldivndvdslt 11632 hashgcdlem 11903 tgtop11 12245 sinq12gt0 12911 |
Copyright terms: Public domain | W3C validator |