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  3838  brelrng  5925  fpr3g  8285  frrlem4  8289  dif1enlem  9155  php3  9204  div2sub  12065  nn0p1elfzo  13759  ssfzo12  13816  modltm1p1mod  13988  hashgt23el  14490  revpfxsfxrev  14838  repswpfx  14857  abssubge0  15416  qredeu  16749  abvne0  20986  pridln1  21532  slesolinvbi  22907  basgen2  23215  fcfval  24260  nmne0  24846  ovolfsf  25700  logbprmirr  27034  lgssq  27574  lgssq2  27575  colinearalg  29368  usgr0v  29702  frgr0vb  30744  nv1  31157  adjeq  32417  ordtypeon  35596  areacirc  38463  fvopabf4g  38473  exidreslem  38628  hgmapvvlem3  42799  iocmbl  44055  iunconnlem2  45758  ssfz12  48203  m1modmmod  48253