Theorem biimp3ar 1470

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 809	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
3	2	3imp 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  rmoi  3882  brelrng  5933  fpr3g  8254  frrlem4  8258  dif1enlem  9141  dif1enlemOLD  9142  php3  9197  div2sub  12023  nn0p1elfzo  13659  ssfzo12  13709  modltm1p1mod  13872  hashgt23el  14368  repswpfx  14719  abssubge0  15258  qredeu  16579  abvne0  20386  slesolinvbi  22114  basgen2  22423  fcfval  23468  nmne0  24059  ovolfsf  24919  logbprmirr  26230  lgssq  26769  lgssq2  26770  colinearalg  28097  usgr0v  28427  frgr0vb  29445  nv1  29855  adjeq  31115  pridln1  32476  revpfxsfxrev  34001  areacirc  36449  fvopabf4g  36458  exidreslem  36614  hgmapvvlem3  40665  iocmbl  41797  iunconnlem2  43531  ssfz12  45858  m1modmmod  46919