Theorem biimp3a 1356

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

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

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 982

This theorem is referenced by:  nnawordex  6596  div2subap  8883  nn0addge1  9314  nn0addge2  9315  nn0sub2  9418  eluzp1p1  9646  uznn0sub  9652  iocssre  10047  icossre  10048  iccssre  10049  lincmb01cmp  10097  iccf1o  10098  fzosplitprm1  10329  subfzo0  10337  modfzo0difsn  10506  efltim  11882  fldivndvdslt  12121  prmdiv  12430  hashgcdlem  12433  vfermltl  12447  coprimeprodsq  12453  pythagtrip  12479  difsqpwdvds  12534  tgtop11  14420  sinq12gt0  15174  gausslemma2dlem1a  15407