Theorem simplbi2 504

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  simplbi2com  506  sspss  4055  neldif  4087  reuss2  4278  pssdifn0  4320  dfiun2g  4986  elinxp  6003  ordunidif  6392  eceqoveq  8799  infxpenlem  9966  ackbij1lem18  10189  isf32lem2  10308  ingru  10770  indpi  10862  nqereu  10884  elpq  12973  elfz0ubfz0  13634  elfzmlbp  13641  elfzo0z  13704  fzofzim  13712  fzo1fzo0n0  13718  elfzodifsumelfzo  13734  swrdswrd  14715  swrdccatin1  14735  swrd2lsw  14962  p1modz1  16276  dfgcd2  16563  algcvga  16596  pcprendvds  16859  restntr  23222  filconn  23923  filssufilg  23951  ufileu  23959  ufilen  23970  alexsubALTlem3  24089  blcld  24545  causs  25340  itg2addlem  25800  rplogsum  27568  ltsres  27703  wlkonl1iedg  29810  trlf1  29843  spthdifv  29879  upgrwlkdvde  29883  usgr2pth  29910  pthdlem2  29914  uspgrn2crct  29954  crctcshwlkn0  29967  clwlkclwwlklem2  30148  clwwlknon0  30241  3spthd  30324  ofpreima2  32818  esumpinfval  34331  eulerpartlemf  34628  fin2so  38070  fdc  38208  lshpcmp  39576  lfl1  39658  frege124d  44301  onfrALTlem2  45086  3ornot23VD  45386  ordelordALTVD  45406  onfrALTlem2VD  45428  ndmaovass  47764  elfz2z  47873  lighneallem4  48183