Theorem biimp3ar 1472

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 810	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
3	2	3imp 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

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

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 1088

This theorem is referenced by:  rmoi  3857  brelrng  5908  fpr3g  8267  frrlem4  8271  dif1enlem  9126  dif1enlemOLD  9127  php3  9179  div2sub  12014  nn0p1elfzo  13670  ssfzo12  13727  modltm1p1mod  13895  hashgt23el  14396  repswpfx  14757  abssubge0  15301  qredeu  16635  abvne0  20735  slesolinvbi  22575  basgen2  22883  fcfval  23927  nmne0  24514  ovolfsf  25379  logbprmirr  26713  lgssq  27255  lgssq2  27256  colinearalg  28844  usgr0v  29175  frgr0vb  30199  nv1  30611  adjeq  31871  pridln1  33421  revpfxsfxrev  35110  areacirc  37714  fvopabf4g  37723  exidreslem  37878  hgmapvvlem3  41926  iocmbl  43209  iunconnlem2  44931  ssfz12  47319  m1modmmod  47363