Theorem biimp3a 1471

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  9138  nn0addge1  12447  nn0addge2  12448  nn0sub2  12553  eluzp1p1  12779  uznn0sub  12786  uzinfi  12841  iocssre  13343  icossre  13344  iccssre  13345  lincmb01cmp  13411  iccf1o  13412  fzosplitprm1  13694  subfzo0  13708  modfzo0difsn  13866  hashprb  14320  pfxpfx  14631  eflt  16042  fldivndvdslt  16343  prmdiv  16712  hashgcdlem  16715  vfermltl  16729  coprimeprodsq  16736  pythagtrip  16762  difsqpwdvds  16815  cshwshashlem2  17024  odinf  19492  odcl2  19494  rnghmresel  20553  rhmresel  20582  slesolex  22626  tgtop11  22926  restntr  23126  hauscmplem  23350  icchmeo  24894  icchmeoOLD  24895  pi1xfr  25011  sinq12gt0  26472  tanord1  26502  gausslemma2dlem1a  27332  ltsn0  27902  onltn0s  28354  pw2cut  28456  axsegconlem6  28995  lfuhgr1v0e  29327  crctcshwlkn0lem6  29888  crctcshwlkn0lem7  29889  clwlkclwwlkf1lem2  30080  s2elclwwlknon2  30179  eucrctshift  30318  eucrct2eupth  30320  nv1  30750  lnolin  30829  br8d  32686  fzm1ne1  32868  ismntd  33066  mntf  33067  cycpmco2lem6  33213  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemrv2  34679  fisshasheq  35309  br8  35950  br6  35951  br4  35952  bj-imdiridlem  37390  ismtyima  38004  ismtybndlem  38007  ghomlinOLD  38089  ghomidOLD  38090  cvrcmp2  39544  atcvrj2  39693  1cvratex  39733  lplnric  39812  lplnri1  39813  lnatexN  40039  ltrnateq  40441  ltrnatneq  40442  cdleme46f2g2  40753  cdleme46f2g1  40754  dibelval1st  41409  dibelval2nd  41412  dicelval1sta  41447  hlhilphllem  42219  jm2.17b  43203  bi123impia  44731  sineq0ALT  45177  eliccre  45751  ioomidp  45760  smfinflem  47061  submodlt  47596  iccpartiltu  47668  goldbachthlem1  47791  evengpop3  48044  gpgcubic  48325  gpg5nbgr3star  48327  itcovalsuc  48913