Theorem biimp3a 1382

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

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

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 1007

This theorem is referenced by:  nnawordex  6762  div2subap  9111  nn0addge1  9542  nn0addge2  9543  nn0sub2  9651  eluzp1p1  9880  uznn0sub  9886  iocssre  10286  icossre  10287  iccssre  10288  lincmb01cmp  10336  iccf1o  10338  fzosplitprm1  10580  subfzo0  10588  modfzo0difsn  10757  pfxpfx  11400  efltim  12384  fldivndvdslt  12623  prmdiv  12932  hashgcdlem  12935  vfermltl  12949  coprimeprodsq  12955  pythagtrip  12981  difsqpwdvds  13036  tgtop11  14941  sinq12gt0  15695  gausslemma2dlem1a  15931  s2elclwwlknon2  16431