Theorem simplbi2 655

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  simplbi2com  657  sspss  3706  neldif  3735  reuss2  3907  pssdifn0  3944  ordunidif  5773  eceqoveq  7853  infxpenlem  8836  ackbij1lem18  9059  isf32lem2  9176  ingru  9637  indpi  9729  nqereu  9751  elfz0ubfz0  12443  elfzmlbp  12450  elfzo0z  12509  fzofzim  12514  fzo1fzo0n0  12518  elfzodifsumelfzo  12533  2swrd1eqwrdeq  13454  swrdswrd  13460  swrdccatin1  13483  swrd2lsw  13695  dfgcd2  15263  algcvga  15292  pcprendvds  15545  restntr  20986  filconn  21687  filssufilg  21715  ufileu  21723  ufilen  21734  alexsubALTlem3  21853  blcld  22310  causs  23096  itg2addlem  23525  rplogsum  25216  wlkonl1iedg  26561  trlf1  26595  spthdifv  26629  upgrwlkdvde  26633  usgr2pth  26660  pthdlem2  26664  uspgrn2crct  26700  crctcshwlkn0  26713  clwlkclwwlklem2  26901  3spthd  27036  ofpreima2  29466  esumpinfval  30135  eulerpartlemf  30432  sltres  31815  bj-elid2  33086  fin2so  33396  fdc  33541  lshpcmp  34275  lfl1  34357  frege124d  38053  onfrALTlem2  38761  3ornot23VD  39082  ordelordALTVD  39103  onfrALTlem2VD  39125  ndmaovass  41286  elfz2z  41325  lighneallem4  41527