Theorem biimp3ar 1469

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 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  3900  brelrng  5955  fpr3g  8309  frrlem4  8313  dif1enlem  9195  dif1enlemOLD  9196  php3  9247  div2sub  12090  nn0p1elfzo  13739  ssfzo12  13795  modltm1p1mod  13961  hashgt23el  14460  repswpfx  14820  abssubge0  15363  qredeu  16692  abvne0  20837  slesolinvbi  22703  basgen2  23012  fcfval  24057  nmne0  24648  ovolfsf  25520  logbprmirr  26854  lgssq  27396  lgssq2  27397  colinearalg  28940  usgr0v  29273  frgr0vb  30292  nv1  30704  adjeq  31964  pridln1  33451  revpfxsfxrev  35100  areacirc  37700  fvopabf4g  37709  exidreslem  37864  hgmapvvlem3  41908  iocmbl  43202  iunconnlem2  44933  ssfz12  47264  m1modmmod  48371