Theorem simplbi2 503

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simplbi2com  505  sspss  4076  neldif  4106  reuss2  4283  pssdifn0  4325  elinxp  5890  ordunidif  6239  eceqoveq  8402  infxpenlem  9439  ackbij1lem18  9659  isf32lem2  9776  ingru  10237  indpi  10329  nqereu  10351  elpq  12375  elfz0ubfz0  13012  elfzmlbp  13019  elfzo0z  13080  fzofzim  13085  fzo1fzo0n0  13089  elfzodifsumelfzo  13104  swrdswrd  14067  swrdccatin1  14087  swrd2lsw  14314  p1modz1  15614  dfgcd2  15894  algcvga  15923  pcprendvds  16177  restntr  21790  filconn  22491  filssufilg  22519  ufileu  22527  ufilen  22538  alexsubALTlem3  22657  blcld  23115  causs  23901  itg2addlem  24359  rplogsum  26103  wlkonl1iedg  27447  trlf1  27480  spthdifv  27514  upgrwlkdvde  27518  usgr2pth  27545  pthdlem2  27549  uspgrn2crct  27586  crctcshwlkn0  27599  clwlkclwwlklem2  27778  clwwlknon0  27872  3spthd  27955  ofpreima2  30411  esumpinfval  31332  eulerpartlemf  31628  sltres  33169  fin2so  34894  fdc  35035  lshpcmp  36139  lfl1  36221  frege124d  40126  onfrALTlem2  40900  3ornot23VD  41201  ordelordALTVD  41221  onfrALTlem2VD  41243  ndmaovass  43425  elfz2z  43535  lighneallem4  43795