Theorem biimp3a 1281

Description: Infer implication from a logical equivalence. Similar to biimpa 290. (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 290	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1138	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∧ w3a 924

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

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  nnawordex  6285  div2subap  8300  nn0addge1  8717  nn0addge2  8718  nn0sub2  8818  eluzp1p1  9042  uznn0sub  9048  iocssre  9369  icossre  9370  iccssre  9371  lincmb01cmp  9418  iccf1o  9419  fzosplitprm1  9641  subfzo0  9649  modfzo0difsn  9798  efltim  10984  fldivndvdslt  11209  hashgcdlem  11477