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  6696  div2subap  9016  nn0addge1  9447  nn0addge2  9448  nn0sub2  9552  eluzp1p1  9781  uznn0sub  9787  iocssre  10187  icossre  10188  iccssre  10189  lincmb01cmp  10237  iccf1o  10238  fzosplitprm1  10479  subfzo0  10487  modfzo0difsn  10656  pfxpfx  11288  efltim  12258  fldivndvdslt  12497  prmdiv  12806  hashgcdlem  12809  vfermltl  12823  coprimeprodsq  12829  pythagtrip  12855  difsqpwdvds  12910  tgtop11  14799  sinq12gt0  15553  gausslemma2dlem1a  15786  s2elclwwlknon2  16286