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  6532  div2subap  8796  nn0addge1  9224  nn0addge2  9225  nn0sub2  9328  eluzp1p1  9555  uznn0sub  9561  iocssre  9955  icossre  9956  iccssre  9957  lincmb01cmp  10005  iccf1o  10006  fzosplitprm1  10236  subfzo0  10244  modfzo0difsn  10397  efltim  11708  fldivndvdslt  11942  prmdiv  12237  hashgcdlem  12240  vfermltl  12253  coprimeprodsq  12259  pythagtrip  12285  difsqpwdvds  12339  tgtop11  13615  sinq12gt0  14290