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  4052  neldif  4084  reuss2  4276  pssdifn0  4318  dfiun2g  4980  elinxp  5968  ordunidif  6356  eceqoveq  8746  infxpenlem  9901  ackbij1lem18  10124  isf32lem2  10242  ingru  10703  indpi  10795  nqereu  10817  elpq  12870  elfz0ubfz0  13529  elfzmlbp  13536  elfzo0z  13598  fzofzim  13606  fzo1fzo0n0  13612  elfzodifsumelfzo  13628  swrdswrd  14609  swrdccatin1  14629  swrd2lsw  14856  p1modz1  16167  dfgcd2  16454  algcvga  16487  pcprendvds  16749  restntr  23095  filconn  23796  filssufilg  23824  ufileu  23832  ufilen  23843  alexsubALTlem3  23962  blcld  24418  causs  25223  itg2addlem  25684  rplogsum  27463  sltres  27599  wlkonl1iedg  29640  trlf1  29673  spthdifv  29709  upgrwlkdvde  29713  usgr2pth  29740  pthdlem2  29744  uspgrn2crct  29784  crctcshwlkn0  29797  clwlkclwwlklem2  29975  clwwlknon0  30068  3spthd  30151  ofpreima2  32643  esumpinfval  34081  eulerpartlemf  34378  fin2so  37646  fdc  37784  lshpcmp  39026  lfl1  39108  frege124d  43793  onfrALTlem2  44578  3ornot23VD  44878  ordelordALTVD  44898  onfrALTlem2VD  44920  ndmaovass  47236  elfz2z  47345  lighneallem4  47640