Theorem biimp3a 1277

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 1134	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 922

This theorem is referenced by:  nnawordex  6189  nn0addge1  8471  nn0addge2  8472  nn0sub2  8572  eluzp1p1  8795  uznn0sub  8801  iocssre  9122  icossre  9123  iccssre  9124  lincmb01cmp  9171  iccf1o  9172  fzosplitprm1  9390  subfzo0  9398  modfzo0difsn  9547  fldivndvdslt  10560  hashgcdlem  10828