Theorem biimp3ar 1468

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 807	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
3	2	3imp 1109	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  rmoi  3828  brelrng  5847  fpr3g  8085  frrlem4  8089  dif1enlem  8908  php3  8959  div2sub  11783  nn0p1elfzo  13411  ssfzo12  13461  modltm1p1mod  13624  hashgt23el  14120  repswpfx  14479  abssubge0  15020  qredeu  16344  abvne0  20068  slesolinvbi  21811  basgen2  22120  fcfval  23165  nmne0  23756  ovolfsf  24616  logbprmirr  25927  lgssq  26466  lgssq2  26467  colinearalg  27259  usgr0v  27589  frgr0vb  28606  nv1  29016  adjeq  30276  pridln1  31597  revpfxsfxrev  33056  areacirc  35849  fvopabf4g  35858  exidreslem  36014  hgmapvvlem3  39918  iocmbl  41024  iunconnlem2  42508  ssfz12  44758  m1modmmod  45819