Theorem biimp3a 1465

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  nn0addge1  11946  nn0addge2  11947  nn0sub2  12046  eluzp1p1  12273  uznn0sub  12280  uzinfi  12331  iocssre  12819  icossre  12820  iccssre  12821  lincmb01cmp  12884  iccf1o  12885  fzosplitprm1  13150  subfzo0  13162  modfzo0difsn  13314  hashprb  13761  pfxpfx  14072  eflt  15472  fldivndvdslt  15767  prmdiv  16124  hashgcdlem  16127  vfermltl  16140  coprimeprodsq  16147  pythagtrip  16173  difsqpwdvds  16225  cshwshashlem2  16432  odinf  18692  odcl2  18694  slesolex  21293  tgtop11  21592  restntr  21792  hauscmplem  22016  icchmeo  23547  pi1xfr  23661  sinq12gt0  25095  tanord1  25123  gausslemma2dlem1a  25943  axsegconlem6  26710  lfuhgr1v0e  27038  crctcshwlkn0lem6  27595  crctcshwlkn0lem7  27596  clwlkclwwlkf1lem2  27785  s2elclwwlknon2  27885  eucrctshift  28024  eucrct2eupth  28026  nv1  28454  lnolin  28533  br8d  30363  fzm1ne1  30514  cycpmco2lem6  30775  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemrv2  31781  fisshasheq  32354  br8  32994  br6  32995  br4  32996  ismtyima  35083  ismtybndlem  35086  ghomlinOLD  35168  ghomidOLD  35169  cvrcmp2  36422  atcvrj2  36571  1cvratex  36611  lplnric  36690  lplnri1  36691  lnatexN  36917  ltrnateq  37319  ltrnatneq  37320  cdleme46f2g2  37631  cdleme46f2g1  37632  dibelval1st  38287  dibelval2nd  38290  dicelval1sta  38325  hlhilphllem  39097  jm2.17b  39565  bi123impia  40830  sineq0ALT  41278  eliccre  41788  ioomidp  41797  smfinflem  43098  iccpartiltu  43589  goldbachthlem1  43714  evengpop3  43970  rnghmresel  44242  rhmresel  44288