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  6692  div2subap  9007  nn0addge1  9438  nn0addge2  9439  nn0sub2  9543  eluzp1p1  9772  uznn0sub  9778  iocssre  10178  icossre  10179  iccssre  10180  lincmb01cmp  10228  iccf1o  10229  fzosplitprm1  10470  subfzo0  10478  modfzo0difsn  10647  pfxpfx  11279  efltim  12249  fldivndvdslt  12488  prmdiv  12797  hashgcdlem  12800  vfermltl  12814  coprimeprodsq  12820  pythagtrip  12846  difsqpwdvds  12901  tgtop11  14790  sinq12gt0  15544  gausslemma2dlem1a  15777  s2elclwwlknon2  16231