![]() |
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 479. (Contributed by NM, 2-Jan-2009.) |
Ref | Expression |
---|---|
biimp3a.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
biimp3ar | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimp3a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | |
2 | 1 | exbiri 810 | . 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
3 | 2 | 3imp 1112 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 |
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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: rmoi 3885 brelrng 5939 fpr3g 8267 frrlem4 8271 dif1enlem 9153 dif1enlemOLD 9154 php3 9209 div2sub 12036 nn0p1elfzo 13672 ssfzo12 13722 modltm1p1mod 13885 hashgt23el 14381 repswpfx 14732 abssubge0 15271 qredeu 16592 abvne0 20428 slesolinvbi 22175 basgen2 22484 fcfval 23529 nmne0 24120 ovolfsf 24980 logbprmirr 26291 lgssq 26830 lgssq2 26831 colinearalg 28158 usgr0v 28488 frgr0vb 29506 nv1 29916 adjeq 31176 pridln1 32550 revpfxsfxrev 34095 areacirc 36570 fvopabf4g 36579 exidreslem 36734 hgmapvvlem3 40785 iocmbl 41948 iunconnlem2 43682 ssfz12 46009 m1modmmod 47161 |
Copyright terms: Public domain | W3C validator |