Theorem biimp3a 1489

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  vtoclegft  3547  onomeneq  9176  nn0addge1  12521  nn0addge2  12522  nn0sub2  12628  eluzp1p1  12861  uznn0sub  12868  uzinfi  12923  iocssre  13425  icossre  13426  iccssre  13427  lincmb01cmp  13493  iccf1o  13494  fzosplitprm1  13778  subfzo0  13792  modfzo0difsn  13950  hashprb  14404  pfxpfx  14715  eflt  16140  fldivndvdslt  16441  prmdiv  16811  hashgcdlem  16814  vfermltl  16828  coprimeprodsq  16835  pythagtrip  16861  difsqpwdvds  16914  cshwshashlem2  17123  odinf  19594  odcl2  19596  rnghmresel  20657  rhmresel  20686  slesolex  22730  tgtop11  23030  restntr  23230  hauscmplem  23454  icchmeo  24991  pi1xfr  25105  sinq12gt0  26560  tanord1  26590  gausslemma2dlem1a  27417  ltsn0  27987  onltn0s  28439  pw2cut  28541  axsegconlem6  29080  lfuhgr1v0e  29412  crctcshwlkn0lem6  29972  crctcshwlkn0lem7  29973  clwlkclwwlkf1lem2  30164  s2elclwwlknon2  30263  eucrctshift  30402  eucrct2eupth  30404  nv1  30835  lnolin  30914  br8d  32771  fzm1ne1  32951  ismntd  33123  mntf  33124  cycpmco2lem6  33272  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemrv2  34780  fisshasheq  35426  br8  36067  br6  36068  br4  36069  cgsex2gd  37590  bj-imdiridlem  37638  ismtyima  38263  ismtybndlem  38266  ghomlinOLD  38348  ghomidOLD  38349  cvrcmp2  39869  atcvrj2  40018  1cvratex  40058  lplnric  40137  lplnri1  40138  lnatexN  40364  ltrnateq  40766  ltrnatneq  40767  cdleme46f2g2  41078  cdleme46f2g1  41079  dibelval1st  41734  dibelval2nd  41737  dicelval1sta  41772  hlhilphllem  42544  jm2.17b  43499  bi123impia  45027  sineq0ALT  45473  eliccre  46042  ioomidp  46051  smfinflem  47352  submodlt  47911  muldvdsfacgt  47941  iccpartiltu  47989  goldbachthlem1  48115  evengpop3  48381  gpgcubic  48662  gpg5nbgr3star  48664  itcovalsuc  49250