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  4030  neldif  4060  reuss2  4246  pssdifn0  4296  elinxp  5918  ordunidif  6299  eceqoveq  8569  infxpenlem  9700  ackbij1lem18  9924  isf32lem2  10041  ingru  10502  indpi  10594  nqereu  10616  elpq  12644  elfz0ubfz0  13289  elfzmlbp  13296  elfzo0z  13357  fzofzim  13362  fzo1fzo0n0  13366  elfzodifsumelfzo  13381  swrdswrd  14346  swrdccatin1  14366  swrd2lsw  14593  p1modz1  15898  dfgcd2  16182  algcvga  16212  pcprendvds  16469  restntr  22241  filconn  22942  filssufilg  22970  ufileu  22978  ufilen  22989  alexsubALTlem3  23108  blcld  23567  causs  24367  itg2addlem  24828  rplogsum  26580  wlkonl1iedg  27935  trlf1  27968  spthdifv  28002  upgrwlkdvde  28006  usgr2pth  28033  pthdlem2  28037  uspgrn2crct  28074  crctcshwlkn0  28087  clwlkclwwlklem2  28265  clwwlknon0  28358  3spthd  28441  ofpreima2  30905  esumpinfval  31941  eulerpartlemf  32237  sltres  33792  fin2so  35691  fdc  35830  lshpcmp  36929  lfl1  37011  frege124d  41258  onfrALTlem2  42055  3ornot23VD  42356  ordelordALTVD  42376  onfrALTlem2VD  42398  ndmaovass  44585  elfz2z  44695  lighneallem4  44950