Theorem biimp3ar 1450

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1069

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 199  df-an 388  df-3an 1071

This theorem is referenced by:  rmoi  3780  brelrng  5659  div2sub  11272  nn0p1elfzo  12901  ssfzo12  12951  modltm1p1mod  13112  hashgt23el  13604  abssubge0  14554  qredeu  15864  abvne0  19332  slesolinvbi  21009  basgen2  21316  fcfval  22360  nmne0  22946  ovolfsf  23790  logbprmirr  25090  lgssq  25630  lgssq2  25631  colinearalg  26414  usgr0v  26741  frgr0vb  27811  nv1  28244  adjeq  29508  fpr3g  32683  frrlem4  32687  areacirc  34468  fvopabf4g  34478  exidreslem  34637  hgmapvvlem3  38546  iocmbl  39256  iunconnlem2  40728  ssfz12  42955  m1modmmod  43984