Theorem simplbi2 501

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  simplbi2com  503  sspss  4040  neldif  4071  reuss2  4261  pssdifn0  4303  dfiun2g  4966  elinxp  5978  ordunidif  6367  eceqoveq  8766  infxpenlem  9933  ackbij1lem18  10156  isf32lem2  10274  ingru  10736  indpi  10828  nqereu  10850  elpq  12923  elfz0ubfz0  13584  elfzmlbp  13591  elfzo0z  13654  fzofzim  13662  fzo1fzo0n0  13668  elfzodifsumelfzo  13684  swrdswrd  14665  swrdccatin1  14685  swrd2lsw  14912  p1modz1  16226  dfgcd2  16513  algcvga  16546  pcprendvds  16809  restntr  23172  filconn  23873  filssufilg  23901  ufileu  23909  ufilen  23920  alexsubALTlem3  24039  blcld  24495  causs  25290  itg2addlem  25750  rplogsum  27515  ltsres  27651  wlkonl1iedg  29757  trlf1  29790  spthdifv  29826  upgrwlkdvde  29830  usgr2pth  29857  pthdlem2  29861  uspgrn2crct  29901  crctcshwlkn0  29914  clwlkclwwlklem2  30095  clwwlknon0  30188  3spthd  30271  ofpreima2  32765  esumpinfval  34264  eulerpartlemf  34561  fin2so  37981  fdc  38119  lshpcmp  39487  lfl1  39569  frege124d  44212  onfrALTlem2  44997  3ornot23VD  45297  ordelordALTVD  45317  onfrALTlem2VD  45339  ndmaovass  47676  elfz2z  47785  lighneallem4  48095