Theorem biimp3a 1345

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

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

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 980

This theorem is referenced by:  nnawordex  6529  div2subap  8793  nn0addge1  9221  nn0addge2  9222  nn0sub2  9325  eluzp1p1  9552  uznn0sub  9558  iocssre  9952  icossre  9953  iccssre  9954  lincmb01cmp  10002  iccf1o  10003  fzosplitprm1  10233  subfzo0  10241  modfzo0difsn  10394  efltim  11705  fldivndvdslt  11939  prmdiv  12234  hashgcdlem  12237  vfermltl  12250  coprimeprodsq  12256  pythagtrip  12282  difsqpwdvds  12336  tgtop11  13546  sinq12gt0  14221