Theorem biimp3a 1477

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  vtoclegft  3527  onomeneq  9138  nn0addge1  12474  nn0addge2  12475  nn0sub2  12581  eluzp1p1  12807  uznn0sub  12814  uzinfi  12869  iocssre  13371  icossre  13372  iccssre  13373  lincmb01cmp  13439  iccf1o  13440  fzosplitprm1  13724  subfzo0  13738  modfzo0difsn  13896  hashprb  14350  pfxpfx  14661  eflt  16075  fldivndvdslt  16376  prmdiv  16746  hashgcdlem  16749  vfermltl  16763  coprimeprodsq  16770  pythagtrip  16796  difsqpwdvds  16849  cshwshashlem2  17058  odinf  19529  odcl2  19531  rnghmresel  20592  rhmresel  20621  slesolex  22665  tgtop11  22965  restntr  23165  hauscmplem  23389  icchmeo  24926  pi1xfr  25040  sinq12gt0  26489  tanord1  26519  gausslemma2dlem1a  27346  ltsn0  27916  onltn0s  28368  pw2cut  28470  axsegconlem6  29009  lfuhgr1v0e  29341  crctcshwlkn0lem6  29901  crctcshwlkn0lem7  29902  clwlkclwwlkf1lem2  30093  s2elclwwlknon2  30192  eucrctshift  30331  eucrct2eupth  30333  nv1  30764  lnolin  30843  br8d  32700  fzm1ne1  32880  ismntd  33063  mntf  33064  cycpmco2lem6  33212  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemrv2  34706  fisshasheq  35343  br8  35984  br6  35985  br4  35986  cgsex2gd  37497  bj-imdiridlem  37545  ismtyima  38170  ismtybndlem  38173  ghomlinOLD  38255  ghomidOLD  38256  cvrcmp2  39776  atcvrj2  39925  1cvratex  39965  lplnric  40044  lplnri1  40045  lnatexN  40271  ltrnateq  40673  ltrnatneq  40674  cdleme46f2g2  40985  cdleme46f2g1  40986  dibelval1st  41641  dibelval2nd  41644  dicelval1sta  41679  hlhilphllem  42451  jm2.17b  43406  bi123impia  44934  sineq0ALT  45380  eliccre  45950  ioomidp  45959  smfinflem  47260  submodlt  47819  muldvdsfacgt  47849  iccpartiltu  47897  goldbachthlem1  48023  evengpop3  48289  gpgcubic  48570  gpg5nbgr3star  48572  itcovalsuc  49158