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  6525  div2subap  8788  nn0addge1  9216  nn0addge2  9217  nn0sub2  9320  eluzp1p1  9547  uznn0sub  9553  iocssre  9947  icossre  9948  iccssre  9949  lincmb01cmp  9997  iccf1o  9998  fzosplitprm1  10227  subfzo0  10235  modfzo0difsn  10388  efltim  11697  fldivndvdslt  11930  prmdiv  12225  hashgcdlem  12228  vfermltl  12241  coprimeprodsq  12247  pythagtrip  12273  difsqpwdvds  12327  tgtop11  13358  sinq12gt0  14033