Theorem biimp3ar 1499

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  rmoi  3838  brelrng  5923  fpr3g  8303  frrlem4  8307  dif1enlem  9175  php3  9224  div2sub  12142  nn0p1elfzo  13837  ssfzo12  13894  modltm1p1mod  14066  hashgt23el  14569  revpfxsfxrev  14917  repswpfx  14936  abssubge0  15495  qredeu  16833  abvne0  21076  pridln1  21624  slesolinvbi  22999  basgen2  23307  fcfval  24352  nmne0  24938  ovolfsf  25792  logbprmirr  27124  lgssq  27664  lgssq2  27665  colinearalg  29488  usgr0v  29822  frgr0vb  30864  nv1  31277  adjeq  32537  ordtypeon  35719  areacirc  38631  fvopabf4g  38656  exidreslem  38811  hgmapvvlem3  42982  iocmbl  44214  iunconnlem2  45916  ssfz12  48383  m1modmmod  48433