Theorem biimp3a 1467

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 1108	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  nn0addge1  12209  nn0addge2  12210  nn0sub2  12311  eluzp1p1  12539  uznn0sub  12546  uzinfi  12597  iocssre  13088  icossre  13089  iccssre  13090  lincmb01cmp  13156  iccf1o  13157  fzosplitprm1  13425  subfzo0  13437  modfzo0difsn  13591  hashprb  14040  pfxpfx  14349  eflt  15754  fldivndvdslt  16051  prmdiv  16414  hashgcdlem  16417  vfermltl  16430  coprimeprodsq  16437  pythagtrip  16463  difsqpwdvds  16516  cshwshashlem2  16726  odinf  19085  odcl2  19087  slesolex  21739  tgtop11  22040  restntr  22241  hauscmplem  22465  icchmeo  24010  pi1xfr  24124  sinq12gt0  25569  tanord1  25598  gausslemma2dlem1a  26418  axsegconlem6  27193  lfuhgr1v0e  27524  crctcshwlkn0lem6  28081  crctcshwlkn0lem7  28082  clwlkclwwlkf1lem2  28270  s2elclwwlknon2  28369  eucrctshift  28508  eucrct2eupth  28510  nv1  28938  lnolin  29017  br8d  30851  fzm1ne1  31012  ismntd  31164  mntf  31165  cycpmco2lem6  31300  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemrv2  32388  fisshasheq  32973  br8  33629  br6  33630  br4  33631  sltn0  34012  bj-imdiridlem  35283  ismtyima  35888  ismtybndlem  35891  ghomlinOLD  35973  ghomidOLD  35974  cvrcmp2  37225  atcvrj2  37374  1cvratex  37414  lplnric  37493  lplnri1  37494  lnatexN  37720  ltrnateq  38122  ltrnatneq  38123  cdleme46f2g2  38434  cdleme46f2g1  38435  dibelval1st  39090  dibelval2nd  39093  dicelval1sta  39128  hlhilphllem  39904  jm2.17b  40699  bi123impia  41998  sineq0ALT  42446  eliccre  42933  ioomidp  42942  smfinflem  44237  iccpartiltu  44762  goldbachthlem1  44885  evengpop3  45138  rnghmresel  45410  rhmresel  45456  itcovalsuc  45901