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  3851  brelrng  5894  fpr3g  8241  frrlem4  8245  dif1enlem  9097  dif1enlemOLD  9098  php3  9150  div2sub  11983  nn0p1elfzo  13639  ssfzo12  13696  modltm1p1mod  13864  hashgt23el  14365  repswpfx  14726  abssubge0  15270  qredeu  16604  abvne0  20704  slesolinvbi  22544  basgen2  22852  fcfval  23896  nmne0  24483  ovolfsf  25348  logbprmirr  26682  lgssq  27224  lgssq2  27225  colinearalg  28813  usgr0v  29144  frgr0vb  30165  nv1  30577  adjeq  31837  pridln1  33387  revpfxsfxrev  35076  areacirc  37680  fvopabf4g  37689  exidreslem  37844  hgmapvvlem3  41892  iocmbl  43175  iunconnlem2  44897  ssfz12  47288  m1modmmod  47332