Theorem biimp3ar 1472

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  rmoi  3803  brelrng  5810  fpr3g  8026  frrlem4  8030  dif1enlem  8838  div2sub  11657  nn0p1elfzo  13285  ssfzo12  13335  modltm1p1mod  13496  hashgt23el  13991  repswpfx  14350  abssubge0  14891  qredeu  16215  abvne0  19863  slesolinvbi  21578  basgen2  21886  fcfval  22930  nmne0  23517  ovolfsf  24368  logbprmirr  25679  lgssq  26218  lgssq2  26219  colinearalg  27001  usgr0v  27329  frgr0vb  28346  nv1  28756  adjeq  30016  pridln1  31332  revpfxsfxrev  32790  areacirc  35607  fvopabf4g  35616  exidreslem  35772  hgmapvvlem3  39676  iocmbl  40747  iunconnlem2  42228  ssfz12  44479  m1modmmod  45540