|   | 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 477. (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 1110 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 | 
| 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: rmoi 3890 brelrng 5951 fpr3g 8311 frrlem4 8315 dif1enlem 9197 dif1enlemOLD 9198 php3 9250 div2sub 12093 nn0p1elfzo 13743 ssfzo12 13799 modltm1p1mod 13965 hashgt23el 14464 repswpfx 14824 abssubge0 15367 qredeu 16696 abvne0 20821 slesolinvbi 22688 basgen2 22997 fcfval 24042 nmne0 24633 ovolfsf 25507 logbprmirr 26840 lgssq 27382 lgssq2 27383 colinearalg 28926 usgr0v 29259 frgr0vb 30283 nv1 30695 adjeq 31955 pridln1 33472 revpfxsfxrev 35122 areacirc 37721 fvopabf4g 37730 exidreslem 37885 hgmapvvlem3 41928 iocmbl 43230 iunconnlem2 44960 ssfz12 47331 m1modmmod 48447 | 
| Copyright terms: Public domain | W3C validator |