Theorem simplbi2 500

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 412	1 ⊢ (𝜓 → (𝜒 → 𝜑))

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

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 396

This theorem is referenced by:  simplbi2com  502  sspss  4099  neldif  4129  reuss2  4315  pssdifn0  4365  dfiun2g  5033  elinxp  6019  ordunidif  6413  eceqoveq  8822  infxpenlem  10014  ackbij1lem18  10238  isf32lem2  10355  ingru  10816  indpi  10908  nqereu  10930  elpq  12966  elfz0ubfz0  13612  elfzmlbp  13619  elfzo0z  13681  fzofzim  13686  fzo1fzo0n0  13690  elfzodifsumelfzo  13705  swrdswrd  14662  swrdccatin1  14682  swrd2lsw  14910  p1modz1  16211  dfgcd2  16495  algcvga  16523  pcprendvds  16780  restntr  22919  filconn  23620  filssufilg  23648  ufileu  23656  ufilen  23667  alexsubALTlem3  23786  blcld  24247  causs  25059  itg2addlem  25521  rplogsum  27281  sltres  27416  wlkonl1iedg  29204  trlf1  29237  spthdifv  29272  upgrwlkdvde  29276  usgr2pth  29303  pthdlem2  29307  uspgrn2crct  29344  crctcshwlkn0  29357  clwlkclwwlklem2  29535  clwwlknon0  29628  3spthd  29711  ofpreima2  32173  esumpinfval  33384  eulerpartlemf  33682  fin2so  36791  fdc  36929  lshpcmp  38174  lfl1  38256  frege124d  42827  onfrALTlem2  43622  3ornot23VD  43923  ordelordALTVD  43943  onfrALTlem2VD  43965  ndmaovass  46225  elfz2z  46334  lighneallem4  46589