Theorem biimp3a 1382

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

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

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 1007

This theorem is referenced by:  nnawordex  6775  div2subap  9128  nn0addge1  9559  nn0addge2  9560  nn0sub2  9668  eluzp1p1  9898  uznn0sub  9904  iocssre  10305  icossre  10306  iccssre  10307  lincmb01cmp  10355  iccf1o  10357  fzosplitprm1  10602  subfzo0  10610  modfzo0difsn  10781  pfxpfx  11425  efltim  12409  fldivndvdslt  12648  prmdiv  12957  hashgcdlem  12960  vfermltl  12974  coprimeprodsq  12980  pythagtrip  13006  difsqpwdvds  13061  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemrv2  13209  tgtop11  15067  sinq12gt0  15821  gausslemma2dlem1a  16057  s2elclwwlknon2  16557