Theorem simplbi2 656

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 449	1 ⊢ (𝜓 → (𝜒 → 𝜑))

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

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 385

This theorem is referenced by:  simplbi2com  658  sspss  3848  neldif  3878  reuss2  4050  pssdifn0  4087  ordunidif  5934  eceqoveq  8019  infxpenlem  9026  ackbij1lem18  9251  isf32lem2  9368  ingru  9829  indpi  9921  nqereu  9943  elfz0ubfz0  12637  elfzmlbp  12644  elfzo0z  12704  fzofzim  12709  fzo1fzo0n0  12713  elfzodifsumelfzo  12728  ccat1st1st  13602  2swrd1eqwrdeq  13654  swrdswrd  13660  swrdccatin1  13683  swrd2lsw  13896  p1modz1  15189  dfgcd2  15465  algcvga  15494  pcprendvds  15747  restntr  21188  filconn  21888  filssufilg  21916  ufileu  21924  ufilen  21935  alexsubALTlem3  22054  blcld  22511  causs  23296  itg2addlem  23724  rplogsum  25415  wlkonl1iedg  26771  trlf1  26805  spthdifv  26839  upgrwlkdvde  26843  usgr2pth  26870  pthdlem2  26874  uspgrn2crct  26911  crctcshwlkn0  26924  clwlkclwwlklem2  27123  clwwlknon0  27240  3spthd  27328  ofpreima2  29775  esumpinfval  30444  eulerpartlemf  30741  sltres  32121  bj-elid2  33397  fin2so  33709  fdc  33854  lshpcmp  34778  lfl1  34860  frege124d  38555  onfrALTlem2  39263  3ornot23VD  39581  ordelordALTVD  39602  onfrALTlem2VD  39624  ndmaovass  41792  elfz2z  41835  lighneallem4  42037