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  6582  div2subap  8856  nn0addge1  9286  nn0addge2  9287  nn0sub2  9390  eluzp1p1  9618  uznn0sub  9624  iocssre  10019  icossre  10020  iccssre  10021  lincmb01cmp  10069  iccf1o  10070  fzosplitprm1  10301  subfzo0  10309  modfzo0difsn  10466  efltim  11841  fldivndvdslt  12076  prmdiv  12373  hashgcdlem  12376  vfermltl  12389  coprimeprodsq  12395  pythagtrip  12421  difsqpwdvds  12476  tgtop11  14244  sinq12gt0  14965  gausslemma2dlem1a  15174