Theorem biimp3a 1471

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  onomeneq  9134  nn0addge1  12438  nn0addge2  12439  nn0sub2  12544  eluzp1p1  12770  uznn0sub  12777  uzinfi  12832  iocssre  13334  icossre  13335  iccssre  13336  lincmb01cmp  13402  iccf1o  13403  fzosplitprm1  13685  subfzo0  13699  modfzo0difsn  13857  hashprb  14311  pfxpfx  14622  eflt  16033  fldivndvdslt  16334  prmdiv  16703  hashgcdlem  16706  vfermltl  16720  coprimeprodsq  16727  pythagtrip  16753  difsqpwdvds  16806  cshwshashlem2  17015  odinf  19483  odcl2  19485  rnghmresel  20544  rhmresel  20573  slesolex  22617  tgtop11  22917  restntr  23117  hauscmplem  23341  icchmeo  24885  icchmeoOLD  24886  pi1xfr  25002  sinq12gt0  26463  tanord1  26493  gausslemma2dlem1a  27323  sltn0  27871  onltn0s  28304  pw2cut  28400  axsegconlem6  28921  lfuhgr1v0e  29253  crctcshwlkn0lem6  29814  crctcshwlkn0lem7  29815  clwlkclwwlkf1lem2  30006  s2elclwwlknon2  30105  eucrctshift  30244  eucrct2eupth  30246  nv1  30676  lnolin  30755  br8d  32612  fzm1ne1  32796  ismntd  32994  mntf  32995  cycpmco2lem6  33141  ballotlemfc0  34578  ballotlemfcc  34579  ballotlemrv2  34607  fisshasheq  35231  br8  35872  br6  35873  br4  35874  bj-imdiridlem  37302  ismtyima  37916  ismtybndlem  37919  ghomlinOLD  38001  ghomidOLD  38002  cvrcmp2  39456  atcvrj2  39605  1cvratex  39645  lplnric  39724  lplnri1  39725  lnatexN  39951  ltrnateq  40353  ltrnatneq  40354  cdleme46f2g2  40665  cdleme46f2g1  40666  dibelval1st  41321  dibelval2nd  41324  dicelval1sta  41359  hlhilphllem  42131  jm2.17b  43118  bi123impia  44647  sineq0ALT  45093  eliccre  45667  ioomidp  45676  smfinflem  46977  submodlt  47512  iccpartiltu  47584  goldbachthlem1  47707  evengpop3  47960  gpgcubic  48241  gpg5nbgr3star  48243  itcovalsuc  48829