Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > biimp3ar | Structured version Visualization version GIF version |
Description: Infer implication from a logical equivalence. Similar to biimpar 501. (Contributed by NM, 2-Jan-2009.) |
Ref | Expression |
---|---|
biimp3a.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
biimp3ar | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp3a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | exbiri 650 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
3 | 2 | 3imp 1249 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 df-3an 1033 |
This theorem is referenced by: rmoi 3496 brelrng 5276 div2sub 10729 nn0p1elfzo 12378 ssfzo12 12427 modltm1p1mod 12584 abssubge0 13915 qredeu 15210 abvne0 18650 slesolinvbi 20306 basgen2 20604 fcfval 21647 nmne0 22233 ovolfsf 23047 lgssq 24862 lgssq2 24863 colinearalg 25590 nv1 26914 adjeq 28178 areacirc 32675 fvopabf4g 32685 exidreslem 32846 hgmapvvlem3 36235 iocmbl 36817 iunconlem2 38193 ssfz12 40351 usgr0v 40467 frgr0vb 41434 m1modmmod 42110 |
Copyright terms: Public domain | W3C validator |