Theorem biimp3a 1498

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is used by:  vtoclegft  3548  onomeneq  9194  nn0addge1  12554  nn0addge2  12555  nn0sub2  12661  eluzp1p1  12894  uznn0sub  12901  uzinfi  12956  iocssre  13458  icossre  13459  iccssre  13460  lincmb01cmp  13526  iccf1o  13527  fzosplitprm1  13812  subfzo0  13826  modfzo0difsn  13984  hashprb  14438  pfxpfx  14750  eflt  16177  fldivndvdslt  16478  prmdiv  16848  hashgcdlem  16851  vfermltl  16865  coprimeprodsq  16872  pythagtrip  16898  difsqpwdvds  16951  cshwshashlem2  17160  odinf  19637  odcl2  19639  rnghmresel  20728  rhmresel  20757  slesolex  22848  tgtop11  23148  restntr  23348  hauscmplem  23572  icchmeo  25109  pi1xfr  25223  sinq12gt0  26681  tanord1  26711  gausslemma2dlem1a  27538  ltsn0  28108  onltn0s  28560  pw2cut  28662  axsegconlem6  29281  lfuhgr1v0e  29613  crctcshwlkn0lem6  30173  crctcshwlkn0lem7  30174  clwlkclwwlkf1lem2  30365  s2elclwwlknon2  30464  eucrctshift  30603  eucrct2eupth  30605  nv1  31036  lnolin  31115  br8d  32962  fzm1ne1  33142  ismntd  33313  mntf  33314  cycpmco2lem6  33460  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemrv2  34921  fisshasheq  35614  br8  36256  br6  36257  br4  36258  cgsex2gd  37809  bj-imdiridlem  37857  ismtyima  38482  ismtybndlem  38485  ghomlinOLD  38567  ghomidOLD  38568  cvrcmp2  40086  atcvrj2  40235  1cvratex  40275  lplnric  40354  lplnri1  40355  lnatexN  40581  ltrnateq  40983  ltrnatneq  40984  cdleme46f2g2  41295  cdleme46f2g1  41296  dibelval1st  41951  dibelval2nd  41954  dicelval1sta  41989  hlhilphllem  42761  jm2.17b  43716  bi123impia  45227  sineq0ALT  45673  eliccre  46249  ioomidp  46258  smfinflem  47559  submodlt  48121  muldvdsfacgt  48151  iccpartiltu  48199  goldbachthlem1  48325  evengpop3  48591  gpgcubic  48872  gpg5nbgr3star  48874  itcovalsuc  49475