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  20739  slesolinvbi  22601  basgen2  22909  fcfval  23953  nmne0  24540  ovolfsf  25405  logbprmirr  26739  lgssq  27281  lgssq2  27282  colinearalg  28890  usgr0v  29221  frgr0vb  30242  nv1  30654  adjeq  31914  pridln1  33407  revpfxsfxrev  35096  areacirc  37700  fvopabf4g  37709  exidreslem  37864  hgmapvvlem3  41912  iocmbl  43195  iunconnlem2  44917  ssfz12  47308  m1modmmod  47352