Theorem biimp3ar 1473

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 811	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
3	2	3imp 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  rmoi  3830  brelrng  5890  fpr3g  8228  frrlem4  8232  dif1enlem  9087  php3  9136  div2sub  11971  nn0p1elfzo  13648  ssfzo12  13705  modltm1p1mod  13876  hashgt23el  14377  repswpfx  14738  abssubge0  15281  qredeu  16618  abvne0  20787  slesolinvbi  22656  basgen2  22964  fcfval  24008  nmne0  24594  ovolfsf  25448  logbprmirr  26773  lgssq  27314  lgssq2  27315  colinearalg  28993  usgr0v  29324  frgr0vb  30348  nv1  30761  adjeq  32021  pridln1  33518  revpfxsfxrev  35314  areacirc  38048  fvopabf4g  38057  exidreslem  38212  hgmapvvlem3  42385  iocmbl  43659  iunconnlem2  45379  ssfz12  47774  m1modmmod  47824