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  9178  nn0addge1  12488  nn0addge2  12489  nn0sub2  12595  eluzp1p1  12821  uznn0sub  12832  uzinfi  12887  iocssre  13388  icossre  13389  iccssre  13390  lincmb01cmp  13456  iccf1o  13457  fzosplitprm1  13738  subfzo0  13750  modfzo0difsn  13908  hashprb  14362  pfxpfx  14673  eflt  16085  fldivndvdslt  16386  prmdiv  16755  hashgcdlem  16758  vfermltl  16772  coprimeprodsq  16779  pythagtrip  16805  difsqpwdvds  16858  cshwshashlem2  17067  odinf  19493  odcl2  19495  rnghmresel  20529  rhmresel  20558  slesolex  22569  tgtop11  22869  restntr  23069  hauscmplem  23293  icchmeo  24838  icchmeoOLD  24839  pi1xfr  24955  sinq12gt0  26416  tanord1  26446  gausslemma2dlem1a  27276  sltn0  27817  onltn0s  28248  pw2cut  28335  axsegconlem6  28849  lfuhgr1v0e  29181  crctcshwlkn0lem6  29745  crctcshwlkn0lem7  29746  clwlkclwwlkf1lem2  29934  s2elclwwlknon2  30033  eucrctshift  30172  eucrct2eupth  30174  nv1  30604  lnolin  30683  br8d  32538  fzm1ne1  32711  ismntd  32910  mntf  32911  cycpmco2lem6  33088  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemrv2  34513  fisshasheq  35102  br8  35743  br6  35744  br4  35745  bj-imdiridlem  37173  ismtyima  37797  ismtybndlem  37800  ghomlinOLD  37882  ghomidOLD  37883  cvrcmp2  39277  atcvrj2  39427  1cvratex  39467  lplnric  39546  lplnri1  39547  lnatexN  39773  ltrnateq  40175  ltrnatneq  40176  cdleme46f2g2  40487  cdleme46f2g1  40488  dibelval1st  41143  dibelval2nd  41146  dicelval1sta  41181  hlhilphllem  41953  jm2.17b  42950  bi123impia  44480  sineq0ALT  44926  eliccre  45503  ioomidp  45512  smfinflem  46815  submodlt  47351  iccpartiltu  47423  goldbachthlem1  47546  evengpop3  47799  gpgcubic  48070  gpg5nbgr3star  48072  itcovalsuc  48656