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  3845  brelrng  5933  fpr3g  8288  frrlem4  8292  dif1enlem  9151  php3  9200  div2sub  12057  nn0p1elfzo  13750  ssfzo12  13807  modltm1p1mod  13979  hashgt23el  14481  revpfxsfxrev  14829  repswpfx  14848  abssubge0  15405  qredeu  16740  abvne0  20974  pridln1  21520  slesolinvbi  22890  basgen2  23198  fcfval  24243  nmne0  24829  ovolfsf  25683  logbprmirr  27014  lgssq  27554  lgssq2  27555  colinearalg  29317  usgr0v  29651  frgr0vb  30687  nv1  31100  adjeq  32360  ordtypeon  35541  areacirc  38423  fvopabf4g  38433  exidreslem  38588  hgmapvvlem3  42759  iocmbl  44000  iunconnlem2  45703  ssfz12  48111  m1modmmod  48161