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  6673  div2subap  8980  nn0addge1  9411  nn0addge2  9412  nn0sub2  9516  eluzp1p1  9744  uznn0sub  9750  iocssre  10145  icossre  10146  iccssre  10147  lincmb01cmp  10195  iccf1o  10196  fzosplitprm1  10435  subfzo0  10443  modfzo0difsn  10612  pfxpfx  11235  efltim  12204  fldivndvdslt  12443  prmdiv  12752  hashgcdlem  12755  vfermltl  12769  coprimeprodsq  12775  pythagtrip  12801  difsqpwdvds  12856  tgtop11  14744  sinq12gt0  15498  gausslemma2dlem1a  15731