Theorem biimp3ar 1500

Description: Infer implication from a logical equivalence. Similar to biimpar 483. (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 823	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
3	2	3imp 1128	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  rmoi  3842  brelrng  5935  fpr3g  8341  frrlem4  8345  dif1enlem  9213  php3  9262  div2sub  12182  nn0p1elfzo  13877  ssfzo12  13934  modltm1p1mod  14106  hashgt23el  14610  revpfxsfxrev  14959  repswpfx  14978  abssubge0  15538  qredeu  16877  abvne0  21127  pridln1  21675  slesolinvbi  23054  basgen2  23362  fcfval  24407  nmne0  24993  ovolfsf  25847  logbprmirr  27181  lgssq  27721  lgssq2  27722  colinearalg  29545  usgr0v  29879  frgr0vb  30921  nv1  31334  adjeq  32594  ordtypeon  35843  areacirc  38899  fvopabf4g  38924  exidreslem  39077  hgmapvvlem3  43248  iocmbl  44476  iunconnlem2  46177  ssfz12  48657  m1modmmod  48707