Theorem simplbi2 504

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  simplbi2com  506  sspss  4005  neldif  4035  reuss2  4217  pssdifn0  4264  elinxp  5861  ordunidif  6217  eceqoveq  8412  infxpenlem  9473  ackbij1lem18  9697  isf32lem2  9814  ingru  10275  indpi  10367  nqereu  10389  elpq  12415  elfz0ubfz0  13060  elfzmlbp  13067  elfzo0z  13128  fzofzim  13133  fzo1fzo0n0  13137  elfzodifsumelfzo  13152  swrdswrd  14114  swrdccatin1  14134  swrd2lsw  14361  p1modz1  15662  dfgcd2  15945  algcvga  15975  pcprendvds  16232  restntr  21882  filconn  22583  filssufilg  22611  ufileu  22619  ufilen  22630  alexsubALTlem3  22749  blcld  23207  causs  23998  itg2addlem  24458  rplogsum  26210  wlkonl1iedg  27554  trlf1  27587  spthdifv  27621  upgrwlkdvde  27625  usgr2pth  27652  pthdlem2  27656  uspgrn2crct  27693  crctcshwlkn0  27706  clwlkclwwlklem2  27884  clwwlknon0  27977  3spthd  28060  ofpreima2  30527  esumpinfval  31560  eulerpartlemf  31856  sltres  33450  fin2so  35346  fdc  35485  lshpcmp  36586  lfl1  36668  frege124d  40857  onfrALTlem2  41647  3ornot23VD  41948  ordelordALTVD  41968  onfrALTlem2VD  41990  ndmaovass  44152  elfz2z  44262  lighneallem4  44517