Theorem biimp3ar 1466

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  rmoi  3875  brelrng  5811  div2sub  11465  nn0p1elfzo  13081  ssfzo12  13131  modltm1p1mod  13292  hashgt23el  13786  repswpfx  14147  abssubge0  14687  qredeu  16002  abvne0  19598  slesolinvbi  21290  basgen2  21597  fcfval  22641  nmne0  23228  ovolfsf  24072  logbprmirr  25374  lgssq  25913  lgssq2  25914  colinearalg  26696  usgr0v  27023  frgr0vb  28042  nv1  28452  adjeq  29712  pridln1  30959  revpfxsfxrev  32362  fpr3g  33122  frrlem4  33126  areacirc  35002  fvopabf4g  35011  exidreslem  35170  hgmapvvlem3  39076  iocmbl  39839  iunconnlem2  41289  ssfz12  43534  m1modmmod  44601