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  4043  neldif  4075  reuss2  4267  pssdifn0  4309  dfiun2g  4973  elinxp  5978  ordunidif  6367  eceqoveq  8762  infxpenlem  9926  ackbij1lem18  10149  isf32lem2  10267  ingru  10729  indpi  10821  nqereu  10843  elpq  12916  elfz0ubfz0  13577  elfzmlbp  13584  elfzo0z  13647  fzofzim  13655  fzo1fzo0n0  13661  elfzodifsumelfzo  13677  swrdswrd  14658  swrdccatin1  14678  swrd2lsw  14905  p1modz1  16219  dfgcd2  16506  algcvga  16539  pcprendvds  16802  restntr  23157  filconn  23858  filssufilg  23886  ufileu  23894  ufilen  23905  alexsubALTlem3  24024  blcld  24480  causs  25275  itg2addlem  25735  rplogsum  27504  ltsres  27640  wlkonl1iedg  29747  trlf1  29780  spthdifv  29816  upgrwlkdvde  29820  usgr2pth  29847  pthdlem2  29851  uspgrn2crct  29891  crctcshwlkn0  29904  clwlkclwwlklem2  30085  clwwlknon0  30178  3spthd  30261  ofpreima2  32754  esumpinfval  34233  eulerpartlemf  34530  fin2so  37942  fdc  38080  lshpcmp  39448  lfl1  39530  frege124d  44206  onfrALTlem2  44991  3ornot23VD  45291  ordelordALTVD  45311  onfrALTlem2VD  45333  ndmaovass  47666  elfz2z  47775  lighneallem4  48085