Theorem biimp3ar 1471

Description: Infer implication from a logical equivalence. Similar to biimpar 479. (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 1112	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  rmoi  3885  brelrng  5939  fpr3g  8267  frrlem4  8271  dif1enlem  9153  dif1enlemOLD  9154  php3  9209  div2sub  12036  nn0p1elfzo  13672  ssfzo12  13722  modltm1p1mod  13885  hashgt23el  14381  repswpfx  14732  abssubge0  15271  qredeu  16592  abvne0  20428  slesolinvbi  22175  basgen2  22484  fcfval  23529  nmne0  24120  ovolfsf  24980  logbprmirr  26291  lgssq  26830  lgssq2  26831  colinearalg  28158  usgr0v  28488  frgr0vb  29506  nv1  29916  adjeq  31176  pridln1  32550  revpfxsfxrev  34095  areacirc  36570  fvopabf4g  36579  exidreslem  36734  hgmapvvlem3  40785  iocmbl  41948  iunconnlem2  43682  ssfz12  46009  m1modmmod  47161