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  3854  brelrng  5905  fpr3g  8264  frrlem4  8268  dif1enlem  9120  dif1enlemOLD  9121  php3  9173  div2sub  12007  nn0p1elfzo  13663  ssfzo12  13720  modltm1p1mod  13888  hashgt23el  14389  repswpfx  14750  abssubge0  15294  qredeu  16628  abvne0  20728  slesolinvbi  22568  basgen2  22876  fcfval  23920  nmne0  24507  ovolfsf  25372  logbprmirr  26706  lgssq  27248  lgssq2  27249  colinearalg  28837  usgr0v  29168  frgr0vb  30192  nv1  30604  adjeq  31864  pridln1  33414  revpfxsfxrev  35103  areacirc  37707  fvopabf4g  37716  exidreslem  37871  hgmapvvlem3  41919  iocmbl  43202  iunconnlem2  44924  ssfz12  47315  m1modmmod  47359