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  9128  nn0addge1  12430  nn0addge2  12431  nn0sub2  12537  eluzp1p1  12763  uznn0sub  12774  uzinfi  12829  iocssre  13330  icossre  13331  iccssre  13332  lincmb01cmp  13398  iccf1o  13399  fzosplitprm1  13680  subfzo0  13692  modfzo0difsn  13850  hashprb  14304  pfxpfx  14614  eflt  16026  fldivndvdslt  16327  prmdiv  16696  hashgcdlem  16699  vfermltl  16713  coprimeprodsq  16720  pythagtrip  16746  difsqpwdvds  16799  cshwshashlem2  17008  odinf  19442  odcl2  19444  rnghmresel  20505  rhmresel  20534  slesolex  22567  tgtop11  22867  restntr  23067  hauscmplem  23291  icchmeo  24836  icchmeoOLD  24837  pi1xfr  24953  sinq12gt0  26414  tanord1  26444  gausslemma2dlem1a  27274  sltn0  27822  onltn0s  28255  pw2cut  28351  axsegconlem6  28871  lfuhgr1v0e  29203  crctcshwlkn0lem6  29764  crctcshwlkn0lem7  29765  clwlkclwwlkf1lem2  29953  s2elclwwlknon2  30052  eucrctshift  30191  eucrct2eupth  30193  nv1  30623  lnolin  30702  br8d  32560  fzm1ne1  32740  ismntd  32935  mntf  32936  cycpmco2lem6  33082  ballotlemfc0  34477  ballotlemfcc  34478  ballotlemrv2  34506  fisshasheq  35108  br8  35749  br6  35750  br4  35751  bj-imdiridlem  37179  ismtyima  37803  ismtybndlem  37806  ghomlinOLD  37888  ghomidOLD  37889  cvrcmp2  39283  atcvrj2  39432  1cvratex  39472  lplnric  39551  lplnri1  39552  lnatexN  39778  ltrnateq  40180  ltrnatneq  40181  cdleme46f2g2  40492  cdleme46f2g1  40493  dibelval1st  41148  dibelval2nd  41151  dicelval1sta  41186  hlhilphllem  41958  jm2.17b  42954  bi123impia  44484  sineq0ALT  44930  eliccre  45506  ioomidp  45515  smfinflem  46818  submodlt  47354  iccpartiltu  47426  goldbachthlem1  47549  evengpop3  47802  gpgcubic  48083  gpg5nbgr3star  48085  itcovalsuc  48672