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  3871  brelrng  5926  fpr3g  8289  frrlem4  8293  dif1enlem  9175  dif1enlemOLD  9176  php3  9228  div2sub  12071  nn0p1elfzo  13724  ssfzo12  13780  modltm1p1mod  13946  hashgt23el  14447  repswpfx  14808  abssubge0  15351  qredeu  16682  abvne0  20784  slesolinvbi  22624  basgen2  22932  fcfval  23976  nmne0  24563  ovolfsf  25429  logbprmirr  26763  lgssq  27305  lgssq2  27306  colinearalg  28894  usgr0v  29225  frgr0vb  30249  nv1  30661  adjeq  31921  pridln1  33463  revpfxsfxrev  35143  areacirc  37742  fvopabf4g  37751  exidreslem  37906  hgmapvvlem3  41949  iocmbl  43204  iunconnlem2  44926  ssfz12  47310  m1modmmod  48468