Theorem biimp3a 1379

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

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

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 1004

This theorem is referenced by:  nnawordex  6683  div2subap  8995  nn0addge1  9426  nn0addge2  9427  nn0sub2  9531  eluzp1p1  9760  uznn0sub  9766  iocssre  10161  icossre  10162  iccssre  10163  lincmb01cmp  10211  iccf1o  10212  fzosplitprm1  10452  subfzo0  10460  modfzo0difsn  10629  pfxpfx  11255  efltim  12224  fldivndvdslt  12463  prmdiv  12772  hashgcdlem  12775  vfermltl  12789  coprimeprodsq  12795  pythagtrip  12821  difsqpwdvds  12876  tgtop11  14765  sinq12gt0  15519  gausslemma2dlem1a  15752