Theorem biimp3a 1468

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  onomeneq  9011  nn0addge1  12279  nn0addge2  12280  nn0sub2  12381  eluzp1p1  12610  uznn0sub  12617  uzinfi  12668  iocssre  13159  icossre  13160  iccssre  13161  lincmb01cmp  13227  iccf1o  13228  fzosplitprm1  13497  subfzo0  13509  modfzo0difsn  13663  hashprb  14112  pfxpfx  14421  eflt  15826  fldivndvdslt  16123  prmdiv  16486  hashgcdlem  16489  vfermltl  16502  coprimeprodsq  16509  pythagtrip  16535  difsqpwdvds  16588  cshwshashlem2  16798  odinf  19170  odcl2  19172  slesolex  21831  tgtop11  22132  restntr  22333  hauscmplem  22557  icchmeo  24104  pi1xfr  24218  sinq12gt0  25664  tanord1  25693  gausslemma2dlem1a  26513  axsegconlem6  27290  lfuhgr1v0e  27621  crctcshwlkn0lem6  28180  crctcshwlkn0lem7  28181  clwlkclwwlkf1lem2  28369  s2elclwwlknon2  28468  eucrctshift  28607  eucrct2eupth  28609  nv1  29037  lnolin  29116  br8d  30950  fzm1ne1  31110  ismntd  31262  mntf  31263  cycpmco2lem6  31398  ballotlemfc0  32459  ballotlemfcc  32460  ballotlemrv2  32488  fisshasheq  33073  br8  33723  br6  33724  br4  33725  sltn0  34085  bj-imdiridlem  35356  ismtyima  35961  ismtybndlem  35964  ghomlinOLD  36046  ghomidOLD  36047  cvrcmp2  37298  atcvrj2  37447  1cvratex  37487  lplnric  37566  lplnri1  37567  lnatexN  37793  ltrnateq  38195  ltrnatneq  38196  cdleme46f2g2  38507  cdleme46f2g1  38508  dibelval1st  39163  dibelval2nd  39166  dicelval1sta  39201  hlhilphllem  39977  jm2.17b  40783  bi123impia  42109  sineq0ALT  42557  eliccre  43043  ioomidp  43052  smfinflem  44350  iccpartiltu  44874  goldbachthlem1  44997  evengpop3  45250  rnghmresel  45522  rhmresel  45568  itcovalsuc  46013