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  3829  brelrng  5896  fpr3g  8235  frrlem4  8239  dif1enlem  9094  php3  9143  div2sub  11980  nn0p1elfzo  13657  ssfzo12  13714  modltm1p1mod  13885  hashgt23el  14386  repswpfx  14747  abssubge0  15290  qredeu  16627  abvne0  20796  slesolinvbi  22646  basgen2  22954  fcfval  23998  nmne0  24584  ovolfsf  25438  logbprmirr  26760  lgssq  27300  lgssq2  27301  colinearalg  28979  usgr0v  29310  frgr0vb  30333  nv1  30746  adjeq  32006  pridln1  33503  revpfxsfxrev  35298  areacirc  38034  fvopabf4g  38043  exidreslem  38198  hgmapvvlem3  42371  iocmbl  43641  iunconnlem2  45361  ssfz12  47762  m1modmmod  47812