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  4094  neldif  4124  reuss2  4310  pssdifn0  4360  dfiun2g  5026  elinxp  6013  ordunidif  6407  eceqoveq  8818  infxpenlem  10010  ackbij1lem18  10234  isf32lem2  10351  ingru  10812  indpi  10904  nqereu  10926  elpq  12963  elfz0ubfz0  13611  elfzmlbp  13618  elfzo0z  13680  fzofzim  13685  fzo1fzo0n0  13689  elfzodifsumelfzo  13704  swrdswrd  14661  swrdccatin1  14681  swrd2lsw  14909  p1modz1  16211  dfgcd2  16495  algcvga  16523  pcprendvds  16782  restntr  23041  filconn  23742  filssufilg  23770  ufileu  23778  ufilen  23789  alexsubALTlem3  23908  blcld  24369  causs  25181  itg2addlem  25643  rplogsum  27415  sltres  27550  wlkonl1iedg  29431  trlf1  29464  spthdifv  29499  upgrwlkdvde  29503  usgr2pth  29530  pthdlem2  29534  uspgrn2crct  29571  crctcshwlkn0  29584  clwlkclwwlklem2  29762  clwwlknon0  29855  3spthd  29938  ofpreima2  32400  esumpinfval  33601  eulerpartlemf  33899  fin2so  36988  fdc  37126  lshpcmp  38371  lfl1  38453  frege124d  43088  onfrALTlem2  43883  3ornot23VD  44184  ordelordALTVD  44204  onfrALTlem2VD  44226  ndmaovass  46486  elfz2z  46595  lighneallem4  46850