Theorem biimp3a 1472

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  vtoclegft  3531  onomeneq  9148  nn0addge1  12483  nn0addge2  12484  nn0sub2  12590  eluzp1p1  12816  uznn0sub  12823  uzinfi  12878  iocssre  13380  icossre  13381  iccssre  13382  lincmb01cmp  13448  iccf1o  13449  fzosplitprm1  13733  subfzo0  13747  modfzo0difsn  13905  hashprb  14359  pfxpfx  14670  eflt  16084  fldivndvdslt  16385  prmdiv  16755  hashgcdlem  16758  vfermltl  16772  coprimeprodsq  16779  pythagtrip  16805  difsqpwdvds  16858  cshwshashlem2  17067  odinf  19538  odcl2  19540  rnghmresel  20597  rhmresel  20626  slesolex  22647  tgtop11  22947  restntr  23147  hauscmplem  23371  icchmeo  24908  pi1xfr  25022  sinq12gt0  26471  tanord1  26501  gausslemma2dlem1a  27328  ltsn0  27898  onltn0s  28350  pw2cut  28452  axsegconlem6  28991  lfuhgr1v0e  29323  crctcshwlkn0lem6  29883  crctcshwlkn0lem7  29884  clwlkclwwlkf1lem2  30075  s2elclwwlknon2  30174  eucrctshift  30313  eucrct2eupth  30315  nv1  30746  lnolin  30825  br8d  32681  fzm1ne1  32861  ismntd  33044  mntf  33045  cycpmco2lem6  33192  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemrv2  34666  fisshasheq  35297  br8  35938  br6  35939  br4  35940  cgsex2gd  37451  bj-imdiridlem  37499  ismtyima  38124  ismtybndlem  38127  ghomlinOLD  38209  ghomidOLD  38210  cvrcmp2  39730  atcvrj2  39879  1cvratex  39919  lplnric  39998  lplnri1  39999  lnatexN  40225  ltrnateq  40627  ltrnatneq  40628  cdleme46f2g2  40939  cdleme46f2g1  40940  dibelval1st  41595  dibelval2nd  41598  dicelval1sta  41633  hlhilphllem  42405  jm2.17b  43389  bi123impia  44917  sineq0ALT  45363  eliccre  45935  ioomidp  45944  smfinflem  47245  submodlt  47804  muldvdsfacgt  47834  iccpartiltu  47882  goldbachthlem1  48008  evengpop3  48274  gpgcubic  48555  gpg5nbgr3star  48557  itcovalsuc  49143