Theorem biimp3ar 1496

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  rmoi  3853  brelrng  5932  fpr3g  8282  frrlem4  8286  dif1enlem  9144  php3  9193  div2sub  12040  nn0p1elfzo  13731  ssfzo12  13788  modltm1p1mod  13959  hashgt23el  14461  repswpfx  14822  abssubge0  15379  qredeu  16716  abvne0  20900  pridln1  21439  slesolinvbi  22807  basgen2  23115  fcfval  24159  nmne0  24745  ovolfsf  25599  logbprmirr  26927  lgssq  27467  lgssq2  27468  colinearalg  29201  usgr0v  29532  frgr0vb  30555  nv1  30968  adjeq  32228  ordtypeon  35424  revpfxsfxrev  35506  areacirc  38252  fvopabf4g  38261  exidreslem  38416  hgmapvvlem3  42589  iocmbl  43832  iunconnlem2  45535  ssfz12  47940  m1modmmod  47990