Theorem biimp3a 1432

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  nn0addge1  11339  nn0addge2  11340  nn0sub2  11438  eluzp1p1  11713  uznn0sub  11719  uzinfi  11768  iocssre  12253  icossre  12254  iccssre  12255  lincmb01cmp  12315  iccf1o  12316  fzosplitprm1  12578  subfzo0  12590  modfzo0difsn  12742  hashprb  13185  swrd0fv  13439  eflt  14847  fldivndvdslt  15138  prmdiv  15490  hashgcdlem  15493  vfermltl  15506  coprimeprodsq  15513  pythagtrip  15539  difsqpwdvds  15591  cshwshashlem2  15803  odinf  17980  odcl2  17982  slesolex  20488  tgtop11  20786  restntr  20986  hauscmplem  21209  icchmeo  22740  pi1xfr  22855  sinq12gt0  24259  tanord1  24283  gausslemma2dlem1a  25090  axsegconlem6  25802  lfuhgr1v0e  26146  crctcshwlkn0lem6  26707  crctcshwlkn0lem7  26708  eucrctshift  27103  eucrct2eupth  27105  nv1  27530  lnolin  27609  br8d  29422  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemrv2  30583  br8  31646  br6  31647  br4  31648  ismtyima  33602  ismtybndlem  33605  ghomlinOLD  33687  ghomidOLD  33688  cvrcmp2  34571  atcvrj2  34719  1cvratex  34759  lplnric  34838  lplnri1  34839  lnatexN  35065  ltrnateq  35468  ltrnatneq  35469  cdleme46f2g2  35781  cdleme46f2g1  35782  dibelval1st  36438  dibelval2nd  36441  dicelval1sta  36476  hlhilphllem  37251  jm2.17b  37528  bi123impia  38695  sineq0ALT  39173  eliccre  39728  ioomidp  39740  smfinflem  41023  iccpartiltu  41358  pfxpfx  41415  repswpfx  41436  goldbachthlem1  41457  fmtnoprmfac1lem  41476  evengpop3  41686  rnghmresel  41964  rhmresel  42010