Theorem biimp3a 1471

Description: Infer implication from a logical equivalence. Similar to biimpa 480. (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 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1112	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091

This theorem is referenced by:  nn0addge1  12101  nn0addge2  12102  nn0sub2  12203  eluzp1p1  12431  uznn0sub  12438  uzinfi  12489  iocssre  12980  icossre  12981  iccssre  12982  lincmb01cmp  13048  iccf1o  13049  fzosplitprm1  13317  subfzo0  13329  modfzo0difsn  13481  hashprb  13929  pfxpfx  14238  eflt  15641  fldivndvdslt  15938  prmdiv  16301  hashgcdlem  16304  vfermltl  16317  coprimeprodsq  16324  pythagtrip  16350  difsqpwdvds  16403  cshwshashlem2  16613  odinf  18908  odcl2  18910  slesolex  21533  tgtop11  21833  restntr  22033  hauscmplem  22257  icchmeo  23792  pi1xfr  23906  sinq12gt0  25351  tanord1  25380  gausslemma2dlem1a  26200  axsegconlem6  26967  lfuhgr1v0e  27296  crctcshwlkn0lem6  27853  crctcshwlkn0lem7  27854  clwlkclwwlkf1lem2  28042  s2elclwwlknon2  28141  eucrctshift  28280  eucrct2eupth  28282  nv1  28710  lnolin  28789  br8d  30623  fzm1ne1  30784  ismntd  30935  mntf  30936  cycpmco2lem6  31071  ballotlemfc0  32125  ballotlemfcc  32126  ballotlemrv2  32154  fisshasheq  32740  br8  33393  br6  33394  br4  33395  sltn0  33771  bj-imdiridlem  35040  ismtyima  35647  ismtybndlem  35650  ghomlinOLD  35732  ghomidOLD  35733  cvrcmp2  36984  atcvrj2  37133  1cvratex  37173  lplnric  37252  lplnri1  37253  lnatexN  37479  ltrnateq  37881  ltrnatneq  37882  cdleme46f2g2  38193  cdleme46f2g1  38194  dibelval1st  38849  dibelval2nd  38852  dicelval1sta  38887  hlhilphllem  39659  jm2.17b  40427  bi123impia  41723  sineq0ALT  42171  eliccre  42659  ioomidp  42668  smfinflem  43965  iccpartiltu  44490  goldbachthlem1  44613  evengpop3  44866  rnghmresel  45138  rhmresel  45184  itcovalsuc  45629