![]() |
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 296. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
biimp3a.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
biimp3a | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp3a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | biimpa 296 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | 3impa 1194 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: nnawordex 6527 div2subap 8790 nn0addge1 9218 nn0addge2 9219 nn0sub2 9322 eluzp1p1 9549 uznn0sub 9555 iocssre 9949 icossre 9950 iccssre 9951 lincmb01cmp 9999 iccf1o 10000 fzosplitprm1 10229 subfzo0 10237 modfzo0difsn 10390 efltim 11699 fldivndvdslt 11932 prmdiv 12227 hashgcdlem 12230 vfermltl 12243 coprimeprodsq 12249 pythagtrip 12275 difsqpwdvds 12329 tgtop11 13447 sinq12gt0 14122 |
Copyright terms: Public domain | W3C validator |