Theorem biimp3a 1382

Description: Infer implication from a logical equivalence. Similar to biimpa 296. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
biimp3a.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
biimp3a	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem biimp3a

Step	Hyp	Ref	Expression
1		biimp3a.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	biimpa 296	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1221	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  nnawordex  6740  div2subap  9059  nn0addge1  9490  nn0addge2  9491  nn0sub2  9597  eluzp1p1  9826  uznn0sub  9832  iocssre  10232  icossre  10233  iccssre  10234  lincmb01cmp  10282  iccf1o  10284  fzosplitprm1  10526  subfzo0  10534  modfzo0difsn  10703  pfxpfx  11338  efltim  12322  fldivndvdslt  12561  prmdiv  12870  hashgcdlem  12873  vfermltl  12887  coprimeprodsq  12893  pythagtrip  12919  difsqpwdvds  12974  tgtop11  14870  sinq12gt0  15624  gausslemma2dlem1a  15860  s2elclwwlknon2  16360