Theorem simplbi2 500

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simplbi2com  502  sspss  4051  neldif  4083  reuss2  4275  pssdifn0  4317  dfiun2g  4980  elinxp  5972  ordunidif  6361  eceqoveq  8752  infxpenlem  9911  ackbij1lem18  10134  isf32lem2  10252  ingru  10713  indpi  10805  nqereu  10827  elpq  12875  elfz0ubfz0  13534  elfzmlbp  13541  elfzo0z  13603  fzofzim  13611  fzo1fzo0n0  13617  elfzodifsumelfzo  13633  swrdswrd  14614  swrdccatin1  14634  swrd2lsw  14861  p1modz1  16172  dfgcd2  16459  algcvga  16492  pcprendvds  16754  restntr  23098  filconn  23799  filssufilg  23827  ufileu  23835  ufilen  23846  alexsubALTlem3  23965  blcld  24421  causs  25226  itg2addlem  25687  rplogsum  27466  sltres  27602  wlkonl1iedg  29644  trlf1  29677  spthdifv  29713  upgrwlkdvde  29717  usgr2pth  29744  pthdlem2  29748  uspgrn2crct  29788  crctcshwlkn0  29801  clwlkclwwlklem2  29982  clwwlknon0  30075  3spthd  30158  ofpreima2  32650  esumpinfval  34107  eulerpartlemf  34404  fin2so  37667  fdc  37805  lshpcmp  39107  lfl1  39189  frege124d  43878  onfrALTlem2  44663  3ornot23VD  44963  ordelordALTVD  44983  onfrALTlem2VD  45005  ndmaovass  47330  elfz2z  47439  lighneallem4  47734