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  4125  neldif  4157  reuss2  4345  pssdifn0  4391  dfiun2g  5053  elinxp  6048  ordunidif  6444  eceqoveq  8880  infxpenlem  10082  ackbij1lem18  10305  isf32lem2  10423  ingru  10884  indpi  10976  nqereu  10998  elpq  13040  elfz0ubfz0  13689  elfzmlbp  13696  elfzo0z  13758  fzofzim  13763  fzo1fzo0n0  13767  elfzodifsumelfzo  13782  swrdswrd  14753  swrdccatin1  14773  swrd2lsw  15001  p1modz1  16309  dfgcd2  16593  algcvga  16626  pcprendvds  16887  restntr  23211  filconn  23912  filssufilg  23940  ufileu  23948  ufilen  23959  alexsubALTlem3  24078  blcld  24539  causs  25351  itg2addlem  25813  rplogsum  27589  sltres  27725  wlkonl1iedg  29701  trlf1  29734  spthdifv  29769  upgrwlkdvde  29773  usgr2pth  29800  pthdlem2  29804  uspgrn2crct  29841  crctcshwlkn0  29854  clwlkclwwlklem2  30032  clwwlknon0  30125  3spthd  30208  ofpreima2  32684  esumpinfval  34037  eulerpartlemf  34335  fin2so  37567  fdc  37705  lshpcmp  38944  lfl1  39026  frege124d  43723  onfrALTlem2  44517  3ornot23VD  44818  ordelordALTVD  44838  onfrALTlem2VD  44860  ndmaovass  47121  elfz2z  47230  lighneallem4  47484