Theorem biimp3a 1357

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

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

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 982

This theorem is referenced by:  nnawordex  6605  div2subap  8892  nn0addge1  9323  nn0addge2  9324  nn0sub2  9428  eluzp1p1  9656  uznn0sub  9662  iocssre  10057  icossre  10058  iccssre  10059  lincmb01cmp  10107  iccf1o  10108  fzosplitprm1  10344  subfzo0  10352  modfzo0difsn  10521  efltim  11928  fldivndvdslt  12167  prmdiv  12476  hashgcdlem  12479  vfermltl  12493  coprimeprodsq  12499  pythagtrip  12525  difsqpwdvds  12580  tgtop11  14466  sinq12gt0  15220  gausslemma2dlem1a  15453