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  8815  infxpenlem  10007  ackbij1lem18  10231  isf32lem2  10348  ingru  10809  indpi  10901  nqereu  10923  elpq  12958  elfz0ubfz0  13604  elfzmlbp  13611  elfzo0z  13673  fzofzim  13678  fzo1fzo0n0  13682  elfzodifsumelfzo  13697  swrdswrd  14654  swrdccatin1  14674  swrd2lsw  14902  p1modz1  16203  dfgcd2  16487  algcvga  16515  pcprendvds  16772  restntr  22685  filconn  23386  filssufilg  23414  ufileu  23422  ufilen  23433  alexsubALTlem3  23552  blcld  24013  causs  24814  itg2addlem  25275  rplogsum  27027  sltres  27162  wlkonl1iedg  28919  trlf1  28952  spthdifv  28987  upgrwlkdvde  28991  usgr2pth  29018  pthdlem2  29022  uspgrn2crct  29059  crctcshwlkn0  29072  clwlkclwwlklem2  29250  clwwlknon0  29343  3spthd  29426  ofpreima2  31886  esumpinfval  33066  eulerpartlemf  33364  fin2so  36470  fdc  36608  lshpcmp  37853  lfl1  37935  frege124d  42502  onfrALTlem2  43297  3ornot23VD  43598  ordelordALTVD  43618  onfrALTlem2VD  43640  ndmaovass  45904  elfz2z  46013  lighneallem4  46268