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  4102  neldif  4134  reuss2  4326  pssdifn0  4368  dfiun2g  5030  elinxp  6037  ordunidif  6433  eceqoveq  8862  infxpenlem  10053  ackbij1lem18  10276  isf32lem2  10394  ingru  10855  indpi  10947  nqereu  10969  elpq  13017  elfz0ubfz0  13672  elfzmlbp  13679  elfzo0z  13741  fzofzim  13749  fzo1fzo0n0  13754  elfzodifsumelfzo  13770  swrdswrd  14743  swrdccatin1  14763  swrd2lsw  14991  p1modz1  16297  dfgcd2  16583  algcvga  16616  pcprendvds  16878  restntr  23190  filconn  23891  filssufilg  23919  ufileu  23927  ufilen  23938  alexsubALTlem3  24057  blcld  24518  causs  25332  itg2addlem  25793  rplogsum  27571  sltres  27707  wlkonl1iedg  29683  trlf1  29716  spthdifv  29753  upgrwlkdvde  29757  usgr2pth  29784  pthdlem2  29788  uspgrn2crct  29828  crctcshwlkn0  29841  clwlkclwwlklem2  30019  clwwlknon0  30112  3spthd  30195  ofpreima2  32676  esumpinfval  34074  eulerpartlemf  34372  fin2so  37614  fdc  37752  lshpcmp  38989  lfl1  39071  frege124d  43774  onfrALTlem2  44566  3ornot23VD  44867  ordelordALTVD  44887  onfrALTlem2VD  44909  ndmaovass  47218  elfz2z  47327  lighneallem4  47597