Theorem biimp3a 1358

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

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

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 983

This theorem is referenced by:  nnawordex  6628  div2subap  8930  nn0addge1  9361  nn0addge2  9362  nn0sub2  9466  eluzp1p1  9694  uznn0sub  9700  iocssre  10095  icossre  10096  iccssre  10097  lincmb01cmp  10145  iccf1o  10146  fzosplitprm1  10385  subfzo0  10393  modfzo0difsn  10562  pfxpfx  11184  efltim  12084  fldivndvdslt  12323  prmdiv  12632  hashgcdlem  12635  vfermltl  12649  coprimeprodsq  12655  pythagtrip  12681  difsqpwdvds  12736  tgtop11  14623  sinq12gt0  15377  gausslemma2dlem1a  15610