Theorem biimp3a 1324

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

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

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 965

This theorem is referenced by:  nnawordex  6464  div2subap  8688  nn0addge1  9115  nn0addge2  9116  nn0sub2  9216  eluzp1p1  9443  uznn0sub  9449  iocssre  9835  icossre  9836  iccssre  9837  lincmb01cmp  9885  iccf1o  9886  fzosplitprm1  10111  subfzo0  10119  modfzo0difsn  10272  efltim  11572  fldivndvdslt  11799  hashgcdlem  12070  tgtop11  12415  sinq12gt0  13090