Theorem biimp3ar 1499

Description: Infer implication from a logical equivalence. Similar to biimpar 482. (Contributed by NM, 2-Jan-2009.)

Hypothesis

Ref	Expression
biimp3a.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
biimp3ar	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Proof of Theorem biimp3ar

Step	Hyp	Ref	Expression
1		biimp3a.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	exbiri 822	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
3	2	3imp 1128	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  rmoi  3844  brelrng  5931  fpr3g  8278  frrlem4  8282  dif1enlem  9140  php3  9189  div2sub  12035  nn0p1elfzo  13727  ssfzo12  13784  modltm1p1mod  13955  hashgt23el  14457  repswpfx  14818  abssubge0  15375  qredeu  16711  abvne0  20922  pridln1  21468  slesolinvbi  22838  basgen2  23146  fcfval  24190  nmne0  24776  ovolfsf  25630  logbprmirr  26961  lgssq  27501  lgssq2  27502  colinearalg  29260  usgr0v  29591  frgr0vb  30614  nv1  31027  adjeq  32287  ordtypeon  35481  revpfxsfxrev  35607  areacirc  38384  fvopabf4g  38393  exidreslem  38548  hgmapvvlem3  42719  iocmbl  43960  iunconnlem2  45663  ssfz12  48071  m1modmmod  48121