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  3837  brelrng  5880  fpr3g  8215  frrlem4  8219  dif1enlem  9069  php3  9118  div2sub  11946  nn0p1elfzo  13602  ssfzo12  13659  modltm1p1mod  13830  hashgt23el  14331  repswpfx  14692  abssubge0  15235  qredeu  16569  abvne0  20734  slesolinvbi  22596  basgen2  22904  fcfval  23948  nmne0  24534  ovolfsf  25399  logbprmirr  26733  lgssq  27275  lgssq2  27276  colinearalg  28888  usgr0v  29219  frgr0vb  30243  nv1  30655  adjeq  31915  pridln1  33408  revpfxsfxrev  35160  areacirc  37763  fvopabf4g  37772  exidreslem  37927  hgmapvvlem3  42034  iocmbl  43316  iunconnlem2  45037  ssfz12  47424  m1modmmod  47468