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  6614  div2subap  8909  nn0addge1  9340  nn0addge2  9341  nn0sub2  9445  eluzp1p1  9673  uznn0sub  9679  iocssre  10074  icossre  10075  iccssre  10076  lincmb01cmp  10124  iccf1o  10125  fzosplitprm1  10361  subfzo0  10369  modfzo0difsn  10538  efltim  11951  fldivndvdslt  12190  prmdiv  12499  hashgcdlem  12502  vfermltl  12516  coprimeprodsq  12522  pythagtrip  12548  difsqpwdvds  12603  tgtop11  14490  sinq12gt0  15244  gausslemma2dlem1a  15477