Theorem simplbi2 501

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

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

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 397

This theorem is referenced by:  simplbi2com  503  sspss  4034  neldif  4064  reuss2  4249  pssdifn0  4299  dfiun2g  4960  elinxp  5929  ordunidif  6314  eceqoveq  8611  infxpenlem  9769  ackbij1lem18  9993  isf32lem2  10110  ingru  10571  indpi  10663  nqereu  10685  elpq  12715  elfz0ubfz0  13360  elfzmlbp  13367  elfzo0z  13429  fzofzim  13434  fzo1fzo0n0  13438  elfzodifsumelfzo  13453  swrdswrd  14418  swrdccatin1  14438  swrd2lsw  14665  p1modz1  15970  dfgcd2  16254  algcvga  16284  pcprendvds  16541  restntr  22333  filconn  23034  filssufilg  23062  ufileu  23070  ufilen  23081  alexsubALTlem3  23200  blcld  23661  causs  24462  itg2addlem  24923  rplogsum  26675  wlkonl1iedg  28033  trlf1  28066  spthdifv  28101  upgrwlkdvde  28105  usgr2pth  28132  pthdlem2  28136  uspgrn2crct  28173  crctcshwlkn0  28186  clwlkclwwlklem2  28364  clwwlknon0  28457  3spthd  28540  ofpreima2  31003  esumpinfval  32041  eulerpartlemf  32337  sltres  33865  fin2so  35764  fdc  35903  lshpcmp  37002  lfl1  37084  frege124d  41369  onfrALTlem2  42166  3ornot23VD  42467  ordelordALTVD  42487  onfrALTlem2VD  42509  ndmaovass  44698  elfz2z  44807  lighneallem4  45062