Theorem biimp3a 1345

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

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

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 980

This theorem is referenced by:  nnawordex  6527  div2subap  8790  nn0addge1  9218  nn0addge2  9219  nn0sub2  9322  eluzp1p1  9549  uznn0sub  9555  iocssre  9949  icossre  9950  iccssre  9951  lincmb01cmp  9999  iccf1o  10000  fzosplitprm1  10229  subfzo0  10237  modfzo0difsn  10390  efltim  11699  fldivndvdslt  11932  prmdiv  12227  hashgcdlem  12230  vfermltl  12243  coprimeprodsq  12249  pythagtrip  12275  difsqpwdvds  12329  tgtop11  13447  sinq12gt0  14122