Theorem biimp3a 1381

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

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

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 1006

This theorem is referenced by:  nnawordex  6697  div2subap  9017  nn0addge1  9448  nn0addge2  9449  nn0sub2  9553  eluzp1p1  9782  uznn0sub  9788  iocssre  10188  icossre  10189  iccssre  10190  lincmb01cmp  10238  iccf1o  10239  fzosplitprm1  10481  subfzo0  10489  modfzo0difsn  10658  pfxpfx  11293  efltim  12277  fldivndvdslt  12516  prmdiv  12825  hashgcdlem  12828  vfermltl  12842  coprimeprodsq  12848  pythagtrip  12874  difsqpwdvds  12929  tgtop11  14819  sinq12gt0  15573  gausslemma2dlem1a  15806  s2elclwwlknon2  16306