Theorem simplbi2 654

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  simplbi2com  656  sspss  3684  neldif  3713  reuss2  3883  pssdifn0  3918  ordunidif  5732  eceqoveq  7798  infxpenlem  8780  ackbij1lem18  9003  isf32lem2  9120  ingru  9581  indpi  9673  nqereu  9695  elfz0ubfz0  12384  elfzmlbp  12391  elfzo0z  12450  fzofzim  12455  fzo1fzo0n0  12459  elfzodifsumelfzo  12474  2swrd1eqwrdeq  13392  swrdswrd  13398  swrdccatin1  13420  swrd2lsw  13629  dfgcd2  15187  algcvga  15216  pcprendvds  15469  restntr  20896  filconn  21597  filssufilg  21625  ufileu  21633  ufilen  21644  alexsubALTlem3  21763  blcld  22220  causs  23004  itg2addlem  23431  rplogsum  25116  wlkonl1iedg  26430  trlf1  26464  spthdifv  26498  upgrwlkdvde  26502  usgr2pth  26529  pthdlem2  26533  uspgrn2crct  26569  crctcshwlkn0  26582  clwlkclwwlklem2  26768  3spthd  26902  ofpreima2  29306  esumpinfval  29913  eulerpartlemf  30210  sltres  31515  bj-elid2  32716  fin2so  33025  fdc  33170  lshpcmp  33752  lfl1  33834  frege124d  37531  onfrALTlem2  38240  3ornot23VD  38562  ordelordALTVD  38583  onfrALTlem2VD  38605  ndmaovass  40587  elfz2z  40619  lighneallem4  40823