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 228	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
3	2	ex 412	1 ⊢ (𝜓 → (𝜒 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  simplbi2com  502  sspss  4077  neldif  4109  reuss2  4301  pssdifn0  4343  dfiun2g  5006  elinxp  6006  ordunidif  6402  eceqoveq  8834  infxpenlem  10025  ackbij1lem18  10248  isf32lem2  10366  ingru  10827  indpi  10919  nqereu  10941  elpq  12989  elfz0ubfz0  13647  elfzmlbp  13654  elfzo0z  13716  fzofzim  13724  fzo1fzo0n0  13729  elfzodifsumelfzo  13745  swrdswrd  14721  swrdccatin1  14741  swrd2lsw  14969  p1modz1  16277  dfgcd2  16563  algcvga  16596  pcprendvds  16858  restntr  23118  filconn  23819  filssufilg  23847  ufileu  23855  ufilen  23866  alexsubALTlem3  23985  blcld  24442  causs  25248  itg2addlem  25709  rplogsum  27488  sltres  27624  wlkonl1iedg  29591  trlf1  29624  spthdifv  29661  upgrwlkdvde  29665  usgr2pth  29692  pthdlem2  29696  uspgrn2crct  29736  crctcshwlkn0  29749  clwlkclwwlklem2  29927  clwwlknon0  30020  3spthd  30103  ofpreima2  32590  esumpinfval  34050  eulerpartlemf  34348  fin2so  37577  fdc  37715  lshpcmp  38952  lfl1  39034  frege124d  43732  onfrALTlem2  44519  3ornot23VD  44819  ordelordALTVD  44839  onfrALTlem2VD  44861  ndmaovass  47183  elfz2z  47292  lighneallem4  47572