Theorem simplbi2 506

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simplbi2com  508  sspss  4059  neldif  4091  reuss2  4282  pssdifn0  4326  dfiun2g  4999  elinxp  6023  ordunidif  6418  eceqoveq  8829  infxpenlem  10016  ackbij1lem18  10238  isf32lem2  10356  ingru  10818  indpi  10910  nqereu  10932  elpq  13017  elfz0ubfz0  13679  elfzmlbp  13686  elfzo0z  13749  fzofzim  13757  fzo1fzo0n0  13763  elfzodifsumelfzo  13779  swrdswrd  14766  swrdccatin1  14786  swrd2lsw  15015  p1modz1  16342  dfgcd2  16629  algcvga  16662  pcprendvds  16925  restntr  23376  filconn  24077  filssufilg  24105  ufileu  24113  ufilen  24124  alexsubALTlem3  24243  blcld  24699  causs  25494  itg2addlem  25954  rplogsum  27728  ltsres  27863  wlkonl1iedg  30050  trlf1  30083  spthdifv  30119  upgrwlkdvde  30123  usgr2pth  30150  pthdlem2  30154  uspgrn2crct  30194  crctcshwlkn0  30207  clwlkclwwlklem2  30388  clwwlknon0  30481  3spthd  30564  ofpreima2  33048  esumpinfval  34494  eulerpartlemf  34792  fin2so  38299  fdc  38437  lshpcmp  39803  lfl1  39885  frege124d  44528  onfrALTlem2  45296  3ornot23VD  45596  ordelordALTVD  45616  onfrALTlem2VD  45638  ndmaovass  47984  elfz2z  48093  lighneallem4  48403