Theorem simplbi2 499

Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)

Hypothesis

Ref	Expression
simplbi2.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi2	⊢ (𝜓 → (𝜒 → 𝜑))

Proof of Theorem simplbi2

Step	Hyp	Ref	Expression
1		simplbi2.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpri 227	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
3	2	ex 411	1 ⊢ (𝜓 → (𝜒 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  simplbi2com  501  sspss  4099  neldif  4130  reuss2  4319  pssdifn0  4369  dfiun2g  5037  elinxp  6028  ordunidif  6423  eceqoveq  8849  infxpenlem  10046  ackbij1lem18  10270  isf32lem2  10387  ingru  10848  indpi  10940  nqereu  10962  elpq  12999  elfz0ubfz0  13647  elfzmlbp  13654  elfzo0z  13716  fzofzim  13721  fzo1fzo0n0  13725  elfzodifsumelfzo  13740  swrdswrd  14697  swrdccatin1  14717  swrd2lsw  14945  p1modz1  16247  dfgcd2  16531  algcvga  16559  pcprendvds  16818  restntr  23114  filconn  23815  filssufilg  23843  ufileu  23851  ufilen  23862  alexsubALTlem3  23981  blcld  24442  causs  25254  itg2addlem  25716  rplogsum  27488  sltres  27623  wlkonl1iedg  29507  trlf1  29540  spthdifv  29575  upgrwlkdvde  29579  usgr2pth  29606  pthdlem2  29610  uspgrn2crct  29647  crctcshwlkn0  29660  clwlkclwwlklem2  29838  clwwlknon0  29931  3spthd  30014  ofpreima2  32481  esumpinfval  33733  eulerpartlemf  34031  fin2so  37121  fdc  37259  lshpcmp  38500  lfl1  38582  frege124d  43240  onfrALTlem2  44034  3ornot23VD  44335  ordelordALTVD  44355  onfrALTlem2VD  44377  ndmaovass  46633  elfz2z  46742  lighneallem4  46997