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  3885  brelrng  5940  fpr3g  8272  frrlem4  8276  dif1enlem  9158  dif1enlemOLD  9159  php3  9214  div2sub  12041  nn0p1elfzo  13677  ssfzo12  13727  modltm1p1mod  13890  hashgt23el  14386  repswpfx  14737  abssubge0  15276  qredeu  16597  abvne0  20439  slesolinvbi  22190  basgen2  22499  fcfval  23544  nmne0  24135  ovolfsf  24995  logbprmirr  26308  lgssq  26847  lgssq2  26848  colinearalg  28206  usgr0v  28536  frgr0vb  29554  nv1  29966  adjeq  31226  pridln1  32606  revpfxsfxrev  34175  areacirc  36667  fvopabf4g  36676  exidreslem  36831  hgmapvvlem3  40882  iocmbl  42044  iunconnlem2  43778  ssfz12  46101  m1modmmod  47285