Theorem biimp3a 1323

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  nnawordex  6424  div2subap  8596  nn0addge1  9023  nn0addge2  9024  nn0sub2  9124  eluzp1p1  9351  uznn0sub  9357  iocssre  9736  icossre  9737  iccssre  9738  lincmb01cmp  9786  iccf1o  9787  fzosplitprm1  10011  subfzo0  10019  modfzo0difsn  10168  efltim  11404  fldivndvdslt  11632  hashgcdlem  11903  tgtop11  12245  sinq12gt0  12911