Theorem biimp3ar 1470

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  rmoi  3829  brelrng  5862  fpr3g  8132  frrlem4  8136  dif1enlem  8981  php3  9033  div2sub  11850  nn0p1elfzo  13480  ssfzo12  13530  modltm1p1mod  13693  hashgt23el  14188  repswpfx  14547  abssubge0  15088  qredeu  16412  abvne0  20136  slesolinvbi  21879  basgen2  22188  fcfval  23233  nmne0  23824  ovolfsf  24684  logbprmirr  25995  lgssq  26534  lgssq2  26535  colinearalg  27327  usgr0v  27657  frgr0vb  28676  nv1  29086  adjeq  30346  pridln1  31667  revpfxsfxrev  33126  areacirc  35918  fvopabf4g  35927  exidreslem  36083  hgmapvvlem3  40139  iocmbl  41240  iunconnlem2  42768  ssfz12  45050  m1modmmod  46111