Theorem biimp3ar 1473

Description: Infer implication from a logical equivalence. Similar to biimpar 477. (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 811	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
3	2	3imp 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  rmoi  3830  brelrng  5891  fpr3g  8229  frrlem4  8233  dif1enlem  9088  php3  9137  div2sub  11974  nn0p1elfzo  13651  ssfzo12  13708  modltm1p1mod  13879  hashgt23el  14380  repswpfx  14741  abssubge0  15284  qredeu  16621  abvne0  20790  slesolinvbi  22659  basgen2  22967  fcfval  24011  nmne0  24597  ovolfsf  25451  logbprmirr  26776  lgssq  27317  lgssq2  27318  colinearalg  28996  usgr0v  29327  frgr0vb  30351  nv1  30764  adjeq  32024  pridln1  33521  revpfxsfxrev  35317  areacirc  38051  fvopabf4g  38060  exidreslem  38215  hgmapvvlem3  42388  iocmbl  43662  iunconnlem2  45382  ssfz12  47777  m1modmmod  47827