Theorem biimp3ar 1499

Description: Infer implication from a logical equivalence. Similar to biimpar 483. (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 823	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
3	2	3imp 1128	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  rmoi  3841  brelrng  5927  fpr3g  8314  frrlem4  8318  dif1enlem  9186  php3  9235  div2sub  12152  nn0p1elfzo  13847  ssfzo12  13904  modltm1p1mod  14076  hashgt23el  14579  revpfxsfxrev  14928  repswpfx  14947  abssubge0  15507  qredeu  16845  abvne0  21088  pridln1  21636  slesolinvbi  23011  basgen2  23319  fcfval  24364  nmne0  24950  ovolfsf  25804  logbprmirr  27136  lgssq  27676  lgssq2  27677  colinearalg  29500  usgr0v  29834  frgr0vb  30876  nv1  31289  adjeq  32549  ordtypeon  35779  areacirc  38771  fvopabf4g  38796  exidreslem  38951  hgmapvvlem3  43122  iocmbl  44355  iunconnlem2  46056  ssfz12  48523  m1modmmod  48573