Theorem biimp3a 1379

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

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

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 1004

This theorem is referenced by:  nnawordex  6688  div2subap  9000  nn0addge1  9431  nn0addge2  9432  nn0sub2  9536  eluzp1p1  9765  uznn0sub  9771  iocssre  10166  icossre  10167  iccssre  10168  lincmb01cmp  10216  iccf1o  10217  fzosplitprm1  10457  subfzo0  10465  modfzo0difsn  10634  pfxpfx  11261  efltim  12230  fldivndvdslt  12469  prmdiv  12778  hashgcdlem  12781  vfermltl  12795  coprimeprodsq  12801  pythagtrip  12827  difsqpwdvds  12882  tgtop11  14771  sinq12gt0  15525  gausslemma2dlem1a  15758