Theorem biimp3a 1386

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  nnawordex  6802  div2subap  9170  nn0addge1  9614  nn0addge2  9615  nn0sub2  9723  eluzp1p1  9958  uznn0sub  9964  iocssre  10366  icossre  10367  iccssre  10368  lincmb01cmp  10416  iccf1o  10418  fzosplitprm1  10664  subfzo0  10672  modfzo0difsn  10847  pfxpfx  11496  efltim  12484  fldivndvdslt  12723  prmdiv  13036  hashgcdlem  13039  vfermltl  13053  coprimeprodsq  13059  pythagtrip  13085  difsqpwdvds  13140  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemrv2  13317  tgtop11  15268  sinq12gt0  16023  gausslemma2dlem1a  16343  s2elclwwlknon2  16843