Theorem biimp3ar 1478

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  rmoi  3823  brelrng  5883  fpr3g  8225  frrlem4  8229  dif1enlem  9084  php3  9133  div2sub  11971  nn0p1elfzo  13648  ssfzo12  13705  modltm1p1mod  13876  hashgt23el  14377  repswpfx  14738  abssubge0  15281  qredeu  16618  abvne0  20791  slesolinvbi  22664  basgen2  22972  fcfval  24016  nmne0  24602  ovolfsf  25456  logbprmirr  26778  lgssq  27318  lgssq2  27319  colinearalg  28997  usgr0v  29328  frgr0vb  30351  nv1  30764  adjeq  32024  pridln1  33526  revpfxsfxrev  35344  areacirc  38080  fvopabf4g  38089  exidreslem  38244  hgmapvvlem3  42417  iocmbl  43658  iunconnlem2  45378  ssfz12  47777  m1modmmod  47827