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  9118  nn0addge1  12422  nn0addge2  12423  nn0sub2  12529  eluzp1p1  12755  uznn0sub  12766  uzinfi  12821  iocssre  13322  icossre  13323  iccssre  13324  lincmb01cmp  13390  iccf1o  13391  fzosplitprm1  13673  subfzo0  13687  modfzo0difsn  13845  hashprb  14299  pfxpfx  14610  eflt  16021  fldivndvdslt  16322  prmdiv  16691  hashgcdlem  16694  vfermltl  16708  coprimeprodsq  16715  pythagtrip  16741  difsqpwdvds  16794  cshwshashlem2  17003  odinf  19470  odcl2  19472  rnghmresel  20530  rhmresel  20559  slesolex  22592  tgtop11  22892  restntr  23092  hauscmplem  23316  icchmeo  24860  icchmeoOLD  24861  pi1xfr  24977  sinq12gt0  26438  tanord1  26468  gausslemma2dlem1a  27298  sltn0  27846  onltn0s  28279  pw2cut  28375  axsegconlem6  28895  lfuhgr1v0e  29227  crctcshwlkn0lem6  29788  crctcshwlkn0lem7  29789  clwlkclwwlkf1lem2  29977  s2elclwwlknon2  30076  eucrctshift  30215  eucrct2eupth  30217  nv1  30647  lnolin  30726  br8d  32583  fzm1ne1  32763  ismntd  32957  mntf  32958  cycpmco2lem6  33092  ballotlemfc0  34498  ballotlemfcc  34499  ballotlemrv2  34527  fisshasheq  35151  br8  35792  br6  35793  br4  35794  bj-imdiridlem  37219  ismtyima  37843  ismtybndlem  37846  ghomlinOLD  37928  ghomidOLD  37929  cvrcmp2  39323  atcvrj2  39472  1cvratex  39512  lplnric  39591  lplnri1  39592  lnatexN  39818  ltrnateq  40220  ltrnatneq  40221  cdleme46f2g2  40532  cdleme46f2g1  40533  dibelval1st  41188  dibelval2nd  41191  dicelval1sta  41226  hlhilphllem  41998  jm2.17b  42994  bi123impia  44523  sineq0ALT  44969  eliccre  45545  ioomidp  45554  smfinflem  46855  submodlt  47381  iccpartiltu  47453  goldbachthlem1  47576  evengpop3  47829  gpgcubic  48110  gpg5nbgr3star  48112  itcovalsuc  48699