| 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 1220 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1004 |
| 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 1006 |
| This theorem is referenced by: nnawordex 6697 div2subap 9017 nn0addge1 9448 nn0addge2 9449 nn0sub2 9553 eluzp1p1 9782 uznn0sub 9788 iocssre 10188 icossre 10189 iccssre 10190 lincmb01cmp 10238 iccf1o 10239 fzosplitprm1 10481 subfzo0 10489 modfzo0difsn 10658 pfxpfx 11293 efltim 12264 fldivndvdslt 12503 prmdiv 12812 hashgcdlem 12815 vfermltl 12829 coprimeprodsq 12835 pythagtrip 12861 difsqpwdvds 12916 tgtop11 14806 sinq12gt0 15560 gausslemma2dlem1a 15793 s2elclwwlknon2 16293 |
| Copyright terms: Public domain | W3C validator |