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  3841  brelrng  5890  fpr3g  8227  frrlem4  8231  dif1enlem  9084  php3  9133  div2sub  11966  nn0p1elfzo  13618  ssfzo12  13675  modltm1p1mod  13846  hashgt23el  14347  repswpfx  14708  abssubge0  15251  qredeu  16585  abvne0  20752  slesolinvbi  22625  basgen2  22933  fcfval  23977  nmne0  24563  ovolfsf  25428  logbprmirr  26762  lgssq  27304  lgssq2  27305  colinearalg  28983  usgr0v  29314  frgr0vb  30338  nv1  30750  adjeq  32010  pridln1  33524  revpfxsfxrev  35310  areacirc  37914  fvopabf4g  37923  exidreslem  38078  hgmapvvlem3  42195  iocmbl  43465  iunconnlem2  45185  ssfz12  47570  m1modmmod  47614