Theorem biimp3ar 1471

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  3890  brelrng  5951  fpr3g  8311  frrlem4  8315  dif1enlem  9197  dif1enlemOLD  9198  php3  9250  div2sub  12093  nn0p1elfzo  13743  ssfzo12  13799  modltm1p1mod  13965  hashgt23el  14464  repswpfx  14824  abssubge0  15367  qredeu  16696  abvne0  20821  slesolinvbi  22688  basgen2  22997  fcfval  24042  nmne0  24633  ovolfsf  25507  logbprmirr  26840  lgssq  27382  lgssq2  27383  colinearalg  28926  usgr0v  29259  frgr0vb  30283  nv1  30695  adjeq  31955  pridln1  33472  revpfxsfxrev  35122  areacirc  37721  fvopabf4g  37730  exidreslem  37885  hgmapvvlem3  41928  iocmbl  43230  iunconnlem2  44960  ssfz12  47331  m1modmmod  48447