Theorem biimp3ar 1470

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 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

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

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 1089

This theorem is referenced by:  rmoi  3913  brelrng  5966  fpr3g  8326  frrlem4  8330  dif1enlem  9222  dif1enlemOLD  9223  php3  9275  div2sub  12119  nn0p1elfzo  13759  ssfzo12  13809  modltm1p1mod  13974  hashgt23el  14473  repswpfx  14833  abssubge0  15376  qredeu  16705  abvne0  20842  slesolinvbi  22708  basgen2  23017  fcfval  24062  nmne0  24653  ovolfsf  25525  logbprmirr  26857  lgssq  27399  lgssq2  27400  colinearalg  28943  usgr0v  29276  frgr0vb  30295  nv1  30707  adjeq  31967  pridln1  33436  revpfxsfxrev  35083  areacirc  37673  fvopabf4g  37682  exidreslem  37837  hgmapvvlem3  41882  iocmbl  43174  iunconnlem2  44906  ssfz12  47229  m1modmmod  48255