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 480. (Contributed by NM, 2-Jan-2009.) |
Ref | Expression |
---|---|
biimp3a.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
biimp3ar | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp3a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | exbiri 809 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
3 | 2 | 3imp 1107 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: rmoi 3875 brelrng 5811 div2sub 11465 nn0p1elfzo 13081 ssfzo12 13131 modltm1p1mod 13292 hashgt23el 13786 repswpfx 14147 abssubge0 14687 qredeu 16002 abvne0 19598 slesolinvbi 21290 basgen2 21597 fcfval 22641 nmne0 23228 ovolfsf 24072 logbprmirr 25374 lgssq 25913 lgssq2 25914 colinearalg 26696 usgr0v 27023 frgr0vb 28042 nv1 28452 adjeq 29712 pridln1 30959 revpfxsfxrev 32362 fpr3g 33122 frrlem4 33126 areacirc 35002 fvopabf4g 35011 exidreslem 35170 hgmapvvlem3 39076 iocmbl 39839 iunconnlem2 41289 ssfz12 43534 m1modmmod 44601 |
Copyright terms: Public domain | W3C validator |