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  9184  nn0addge1  12495  nn0addge2  12496  nn0sub2  12602  eluzp1p1  12828  uznn0sub  12839  uzinfi  12894  iocssre  13395  icossre  13396  iccssre  13397  lincmb01cmp  13463  iccf1o  13464  fzosplitprm1  13745  subfzo0  13757  modfzo0difsn  13915  hashprb  14369  pfxpfx  14680  eflt  16092  fldivndvdslt  16393  prmdiv  16762  hashgcdlem  16765  vfermltl  16779  coprimeprodsq  16786  pythagtrip  16812  difsqpwdvds  16865  cshwshashlem2  17074  odinf  19500  odcl2  19502  rnghmresel  20536  rhmresel  20565  slesolex  22576  tgtop11  22876  restntr  23076  hauscmplem  23300  icchmeo  24845  icchmeoOLD  24846  pi1xfr  24962  sinq12gt0  26423  tanord1  26453  gausslemma2dlem1a  27283  sltn0  27824  onltn0s  28255  pw2cut  28342  axsegconlem6  28856  lfuhgr1v0e  29188  crctcshwlkn0lem6  29752  crctcshwlkn0lem7  29753  clwlkclwwlkf1lem2  29941  s2elclwwlknon2  30040  eucrctshift  30179  eucrct2eupth  30181  nv1  30611  lnolin  30690  br8d  32545  fzm1ne1  32718  ismntd  32917  mntf  32918  cycpmco2lem6  33095  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemrv2  34520  fisshasheq  35109  br8  35750  br6  35751  br4  35752  bj-imdiridlem  37180  ismtyima  37804  ismtybndlem  37807  ghomlinOLD  37889  ghomidOLD  37890  cvrcmp2  39284  atcvrj2  39434  1cvratex  39474  lplnric  39553  lplnri1  39554  lnatexN  39780  ltrnateq  40182  ltrnatneq  40183  cdleme46f2g2  40494  cdleme46f2g1  40495  dibelval1st  41150  dibelval2nd  41153  dicelval1sta  41188  hlhilphllem  41960  jm2.17b  42957  bi123impia  44487  sineq0ALT  44933  eliccre  45510  ioomidp  45519  smfinflem  46822  submodlt  47355  iccpartiltu  47427  goldbachthlem1  47550  evengpop3  47803  gpgcubic  48074  gpg5nbgr3star  48076  itcovalsuc  48660