Theorem biimp3a 1499

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  3547  onomeneq  9267  nn0addge1  12692  nn0addge2  12693  nn0sub2  12800  eluzp1p1  13033  uznn0sub  13040  uzinfi  13095  iocssre  13598  icossre  13599  iccssre  13600  lincmb01cmp  13666  iccf1o  13667  fzosplitprm1  13953  subfzo0  13968  modfzo0difsn  14126  hashprb  14582  pfxpfx  14899  eflt  16329  fldivndvdslt  16630  prmdiv  17006  hashgcdlem  17009  vfermltl  17023  coprimeprodsq  17030  pythagtrip  17056  difsqpwdvds  17109  cshwshashlem2  17318  odinf  19828  odcl2  19830  rnghmresel  20923  rhmresel  20952  slesolex  23055  tgtop11  23355  restntr  23555  hauscmplem  23779  icchmeo  25317  pi1xfr  25431  sinq12gt0  26893  tanord1  26922  gausslemma2dlem1a  27749  ltsn0  28349  onltn0s  28801  pw2cut  28903  axsegconlem6  29557  lfuhgr1v0e  29892  crctcshwlkn0lem6  30461  crctcshwlkn0lem7  30462  clwlkclwwlkf1lem2  30653  s2elclwwlknon2  30752  eucrctshift  30901  eucrct2eupth  30903  nv1  31334  lnolin  31413  br8d  33300  fzm1ne1  33476  ismntd  33644  mntf  33645  cycpmco2lem6  33791  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemrv2  35265  fisshasheq  36101  br8  36736  br6  36737  br4  36738  cgsex2gd  38329  bj-imdiridlem  38374  ismtyima  39003  ismtybndlem  39006  ghomlinOLD  39088  ghomidOLD  39089  cvrcmp2  40607  atcvrj2  40756  1cvratex  40796  lplnric  40875  lplnri1  40876  lnatexN  41102  ltrnateq  41504  ltrnatneq  41505  cdleme46f2g2  41816  cdleme46f2g1  41817  dibelval1st  42472  dibelval2nd  42475  dicelval1sta  42510  hlhilphllem  43282  jm2.17b  44234  bi123impia  45733  sineq0ALT  46179  eliccre  46790  ioomidp  46799  smfinflem  48100  submodlt  48699  muldvdsfacgt  48729  iccpartiltu  48777  goldbachthlem1  48903  evengpop3  49169  gpgcubic  49450  gpg5nbgr3star  49452  itcovalsuc  50110