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  4056  neldif  4088  reuss2  4280  pssdifn0  4322  dfiun2g  4987  elinxp  5986  ordunidif  6375  eceqoveq  8771  infxpenlem  9935  ackbij1lem18  10158  isf32lem2  10276  ingru  10738  indpi  10830  nqereu  10852  elpq  12900  elfz0ubfz0  13560  elfzmlbp  13567  elfzo0z  13629  fzofzim  13637  fzo1fzo0n0  13643  elfzodifsumelfzo  13659  swrdswrd  14640  swrdccatin1  14660  swrd2lsw  14887  p1modz1  16198  dfgcd2  16485  algcvga  16518  pcprendvds  16780  restntr  23138  filconn  23839  filssufilg  23867  ufileu  23875  ufilen  23886  alexsubALTlem3  24005  blcld  24461  causs  25266  itg2addlem  25727  rplogsum  27506  ltsres  27642  wlkonl1iedg  29749  trlf1  29782  spthdifv  29818  upgrwlkdvde  29822  usgr2pth  29849  pthdlem2  29853  uspgrn2crct  29893  crctcshwlkn0  29906  clwlkclwwlklem2  30087  clwwlknon0  30180  3spthd  30263  ofpreima2  32755  esumpinfval  34250  eulerpartlemf  34547  fin2so  37852  fdc  37990  lshpcmp  39358  lfl1  39440  frege124d  44111  onfrALTlem2  44896  3ornot23VD  45196  ordelordALTVD  45216  onfrALTlem2VD  45238  ndmaovass  47560  elfz2z  47669  lighneallem4  47964