Theorem biimp3a 1498

Description: Infer implication from a logical equivalence. Similar to biimpa 482. (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 482	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1127	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  vtoclegft  3543  onomeneq  9234  nn0addge1  12657  nn0addge2  12658  nn0sub2  12765  eluzp1p1  12998  uznn0sub  13005  uzinfi  13060  iocssre  13563  icossre  13564  iccssre  13565  lincmb01cmp  13631  iccf1o  13632  fzosplitprm1  13918  subfzo0  13933  modfzo0difsn  14091  hashprb  14546  pfxpfx  14863  eflt  16292  fldivndvdslt  16593  prmdiv  16969  hashgcdlem  16972  vfermltl  16986  coprimeprodsq  16993  pythagtrip  17019  difsqpwdvds  17072  cshwshashlem2  17281  odinf  19784  odcl2  19786  rnghmresel  20879  rhmresel  20908  slesolex  23007  tgtop11  23307  restntr  23507  hauscmplem  23731  icchmeo  25269  pi1xfr  25383  sinq12gt0  26843  tanord1  26872  gausslemma2dlem1a  27699  ltsn0  28299  onltn0s  28751  pw2cut  28853  axsegconlem6  29507  lfuhgr1v0e  29842  crctcshwlkn0lem6  30411  crctcshwlkn0lem7  30412  clwlkclwwlkf1lem2  30603  s2elclwwlknon2  30702  eucrctshift  30851  eucrct2eupth  30853  nv1  31284  lnolin  31363  br8d  33251  fzm1ne1  33428  ismntd  33593  mntf  33594  cycpmco2lem6  33740  ballotlemfc0  35173  ballotlemfcc  35174  ballotlemrv2  35202  fisshasheq  35981  br8  36615  br6  36616  br4  36617  cgsex2gd  38165  bj-imdiridlem  38213  ismtyima  38844  ismtybndlem  38847  ghomlinOLD  38929  ghomidOLD  38930  cvrcmp2  40448  atcvrj2  40597  1cvratex  40637  lplnric  40716  lplnri1  40717  lnatexN  40943  ltrnateq  41345  ltrnatneq  41346  cdleme46f2g2  41657  cdleme46f2g1  41658  dibelval1st  42313  dibelval2nd  42316  dicelval1sta  42351  hlhilphllem  43123  jm2.17b  44075  bi123impia  45580  sineq0ALT  46026  eliccre  46624  ioomidp  46633  smfinflem  47934  submodlt  48533  muldvdsfacgt  48563  iccpartiltu  48611  goldbachthlem1  48737  evengpop3  49003  gpgcubic  49284  gpg5nbgr3star  49286  itcovalsuc  49886