Theorem biimp3a 1468

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  9262  nn0addge1  12569  nn0addge2  12570  nn0sub2  12676  eluzp1p1  12903  uznn0sub  12914  uzinfi  12967  iocssre  13463  icossre  13464  iccssre  13465  lincmb01cmp  13531  iccf1o  13532  fzosplitprm1  13812  subfzo0  13824  modfzo0difsn  13980  hashprb  14432  pfxpfx  14742  eflt  16149  fldivndvdslt  16449  prmdiv  16818  hashgcdlem  16821  vfermltl  16834  coprimeprodsq  16841  pythagtrip  16867  difsqpwdvds  16920  cshwshashlem2  17130  odinf  19595  odcl2  19597  rnghmresel  20636  rhmresel  20665  slesolex  22703  tgtop11  23004  restntr  23205  hauscmplem  23429  icchmeo  24984  icchmeoOLD  24985  pi1xfr  25101  sinq12gt0  26563  tanord1  26593  gausslemma2dlem1a  27423  sltn0  27957  pw2cut  28434  axsegconlem6  28951  lfuhgr1v0e  29285  crctcshwlkn0lem6  29844  crctcshwlkn0lem7  29845  clwlkclwwlkf1lem2  30033  s2elclwwlknon2  30132  eucrctshift  30271  eucrct2eupth  30273  nv1  30703  lnolin  30782  br8d  32629  fzm1ne1  32796  ismntd  32958  mntf  32959  cycpmco2lem6  33133  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemrv2  34502  fisshasheq  35098  br8  35735  br6  35736  br4  35737  bj-imdiridlem  37167  ismtyima  37789  ismtybndlem  37792  ghomlinOLD  37874  ghomidOLD  37875  cvrcmp2  39265  atcvrj2  39415  1cvratex  39455  lplnric  39534  lplnri1  39535  lnatexN  39761  ltrnateq  40163  ltrnatneq  40164  cdleme46f2g2  40475  cdleme46f2g1  40476  dibelval1st  41131  dibelval2nd  41134  dicelval1sta  41169  hlhilphllem  41945  jm2.17b  42949  bi123impia  44486  sineq0ALT  44934  eliccre  45457  ioomidp  45466  smfinflem  46772  submodlt  47289  iccpartiltu  47346  goldbachthlem1  47469  evengpop3  47722  gpgcubic  47969  gpg5nbgr3star  47971  itcovalsuc  48516