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  4068  neldif  4100  reuss2  4292  pssdifn0  4334  dfiun2g  4997  elinxp  5993  ordunidif  6385  eceqoveq  8798  infxpenlem  9973  ackbij1lem18  10196  isf32lem2  10314  ingru  10775  indpi  10867  nqereu  10889  elpq  12941  elfz0ubfz0  13600  elfzmlbp  13607  elfzo0z  13669  fzofzim  13677  fzo1fzo0n0  13683  elfzodifsumelfzo  13699  swrdswrd  14677  swrdccatin1  14697  swrd2lsw  14925  p1modz1  16236  dfgcd2  16523  algcvga  16556  pcprendvds  16818  restntr  23076  filconn  23777  filssufilg  23805  ufileu  23813  ufilen  23824  alexsubALTlem3  23943  blcld  24400  causs  25205  itg2addlem  25666  rplogsum  27445  sltres  27581  wlkonl1iedg  29600  trlf1  29633  spthdifv  29670  upgrwlkdvde  29674  usgr2pth  29701  pthdlem2  29705  uspgrn2crct  29745  crctcshwlkn0  29758  clwlkclwwlklem2  29936  clwwlknon0  30029  3spthd  30112  ofpreima2  32597  esumpinfval  34070  eulerpartlemf  34368  fin2so  37608  fdc  37746  lshpcmp  38988  lfl1  39070  frege124d  43757  onfrALTlem2  44543  3ornot23VD  44843  ordelordALTVD  44863  onfrALTlem2VD  44885  ndmaovass  47211  elfz2z  47320  lighneallem4  47615