Theorem biimp3ar 1472

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  rmoi  3839  brelrng  5888  fpr3g  8225  frrlem4  8229  dif1enlem  9082  php3  9131  div2sub  11964  nn0p1elfzo  13616  ssfzo12  13673  modltm1p1mod  13844  hashgt23el  14345  repswpfx  14706  abssubge0  15249  qredeu  16583  abvne0  20750  slesolinvbi  22623  basgen2  22931  fcfval  23975  nmne0  24561  ovolfsf  25426  logbprmirr  26760  lgssq  27302  lgssq2  27303  colinearalg  28932  usgr0v  29263  frgr0vb  30287  nv1  30699  adjeq  31959  pridln1  33473  revpfxsfxrev  35259  areacirc  37853  fvopabf4g  37862  exidreslem  38017  hgmapvvlem3  42124  iocmbl  43397  iunconnlem2  45117  ssfz12  47502  m1modmmod  47546