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  3843  brelrng  5898  fpr3g  8237  frrlem4  8241  dif1enlem  9096  php3  9145  div2sub  11978  nn0p1elfzo  13630  ssfzo12  13687  modltm1p1mod  13858  hashgt23el  14359  repswpfx  14720  abssubge0  15263  qredeu  16597  abvne0  20764  slesolinvbi  22637  basgen2  22945  fcfval  23989  nmne0  24575  ovolfsf  25440  logbprmirr  26774  lgssq  27316  lgssq2  27317  colinearalg  28995  usgr0v  29326  frgr0vb  30350  nv1  30763  adjeq  32023  pridln1  33536  revpfxsfxrev  35332  areacirc  37964  fvopabf4g  37973  exidreslem  38128  hgmapvvlem3  42301  iocmbl  43570  iunconnlem2  45290  ssfz12  47674  m1modmmod  47718