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  3843  brelrng  5883  fpr3g  8218  frrlem4  8222  dif1enlem  9073  php3  9123  div2sub  11949  nn0p1elfzo  13605  ssfzo12  13662  modltm1p1mod  13830  hashgt23el  14331  repswpfx  14691  abssubge0  15235  qredeu  16569  abvne0  20704  slesolinvbi  22566  basgen2  22874  fcfval  23918  nmne0  24505  ovolfsf  25370  logbprmirr  26704  lgssq  27246  lgssq2  27247  colinearalg  28855  usgr0v  29186  frgr0vb  30207  nv1  30619  adjeq  31879  pridln1  33380  revpfxsfxrev  35093  areacirc  37697  fvopabf4g  37706  exidreslem  37861  hgmapvvlem3  41908  iocmbl  43190  iunconnlem2  44912  ssfz12  47302  m1modmmod  47346