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  4099  neldif  4129  reuss2  4315  pssdifn0  4365  dfiun2g  5033  elinxp  6019  ordunidif  6413  eceqoveq  8818  infxpenlem  10010  ackbij1lem18  10234  isf32lem2  10351  ingru  10812  indpi  10904  nqereu  10926  elpq  12961  elfz0ubfz0  13607  elfzmlbp  13614  elfzo0z  13676  fzofzim  13681  fzo1fzo0n0  13685  elfzodifsumelfzo  13700  swrdswrd  14657  swrdccatin1  14677  swrd2lsw  14905  p1modz1  16206  dfgcd2  16490  algcvga  16518  pcprendvds  16775  restntr  22693  filconn  23394  filssufilg  23422  ufileu  23430  ufilen  23441  alexsubALTlem3  23560  blcld  24021  causs  24822  itg2addlem  25283  rplogsum  27037  sltres  27172  wlkonl1iedg  28960  trlf1  28993  spthdifv  29028  upgrwlkdvde  29032  usgr2pth  29059  pthdlem2  29063  uspgrn2crct  29100  crctcshwlkn0  29113  clwlkclwwlklem2  29291  clwwlknon0  29384  3spthd  29467  ofpreima2  31929  esumpinfval  33140  eulerpartlemf  33438  fin2so  36561  fdc  36699  lshpcmp  37944  lfl1  38026  frege124d  42594  onfrALTlem2  43389  3ornot23VD  43690  ordelordALTVD  43710  onfrALTlem2VD  43732  ndmaovass  45993  elfz2z  46102  lighneallem4  46357