Theorem simplbi2 653

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385

This theorem is referenced by:  simplbi2com  655  sspss  3668  neldif  3697  reuss2  3866  pssdifn0  3898  ordunidif  5690  eceqoveq  7740  infxpenlem  8719  ackbij1lem18  8942  isf32lem2  9059  ingru  9516  indpi  9608  nqereu  9630  elfz0ubfz0  12312  elfzmlbp  12319  elfzo0z  12377  fzofzim  12382  fzo1fzo0n0  12386  elfzodifsumelfzo  12401  2swrd1eqwrdeq  13306  swrdswrd  13312  swrdccatin1  13334  swrd2lsw  13543  dfgcd2  15101  algcvga  15130  pcprendvds  15383  restntr  20796  filcon  21497  filssufilg  21525  ufileu  21533  ufilen  21544  alexsubALTlem3  21663  blcld  22120  causs  22904  itg2addlem  23331  rplogsum  25016  sizeusglecusglem1  26012  clwlkisclwwlklem1  26315  clwwlknwwlkncl  26328  numclwwlk2lem1  26629  ofpreima2  28849  esumpinfval  29462  eulerpartlemf  29759  sltres  31061  bj-elid2  32263  fin2so  32566  fdc  32711  lshpcmp  33293  lfl1  33375  frege124d  37072  onfrALTlem2  37782  3ornot23VD  38104  ordelordALTVD  38125  onfrALTlem2VD  38147  ndmaovass  39935  lighneallem4  40065  elfz2z  40352  wlkOnl1iedg  40873  trlf1  40906  sPthdifv  40939  upgrwlkdvde  40943  usgr2pth  40970  pthdlem2  40974  uspgrn2crct  41011  crctcsh1wlkn0  41024  clwlkclwwlklem2  41209  3spthd  41343