Theorem biimp3ar 1491

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  rmoi  3844  brelrng  5917  fpr3g  8266  frrlem4  8270  dif1enlem  9128  php3  9177  div2sub  12016  nn0p1elfzo  13708  ssfzo12  13765  modltm1p1mod  13936  hashgt23el  14437  repswpfx  14798  abssubge0  15355  qredeu  16692  abvne0  20868  slesolinvbi  22741  basgen2  23049  fcfval  24093  nmne0  24679  ovolfsf  25533  logbprmirr  26861  lgssq  27401  lgssq2  27402  colinearalg  29111  usgr0v  29442  frgr0vb  30465  nv1  30878  adjeq  32138  pridln1  33629  ordtypeon  35386  revpfxsfxrev  35466  areacirc  38212  fvopabf4g  38221  exidreslem  38376  hgmapvvlem3  42549  iocmbl  43790  iunconnlem2  45510  ssfz12  47908  m1modmmod  47958