Theorem biimp3ar 1582

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  rmoi  3671  brelrng  5510  div2sub  11062  nn0p1elfzo  12725  ssfzo12  12775  modltm1p1mod  12936  abssubge0  14286  qredeu  15594  abvne0  19049  slesolinvbi  20709  basgen2  21015  fcfval  22058  nmne0  22644  ovolfsf  23460  lgssq  25282  lgssq2  25283  colinearalg  26010  usgr0v  26353  frgr0vb  27437  nv1  27860  adjeq  29124  frrlem4  32110  areacirc  33836  fvopabf4g  33846  exidreslem  34007  hgmapvvlem3  37737  iocmbl  38318  iunconnlem2  39688  ssfz12  41852  m1modmmod  42844