Theorem simplbi2 506

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simplbi2com  508  sspss  4029  neldif  4070  reuss2  4271  pssdifn0  4315  dfiun2g  4987  elinxp  6007  ordunidif  6413  eceqoveq  8846  infxpenlem  10095  ackbij1lem18  10317  isf32lem2  10435  ingru  10903  indpi  10995  nqereu  11017  elpq  13106  elfz0ubfz0  13769  elfzmlbp  13776  elfzo0z  13839  fzofzim  13847  fzo1fzo0n0  13853  elfzodifsumelfzo  13869  swrdswrd  14858  swrdccatin1  14878  swrd2lsw  15110  p1modz1  16434  dfgcd2  16724  algcvga  16759  pcprendvds  17023  restntr  23505  filconn  24207  filssufilg  24235  ufileu  24243  ufilen  24254  alexsubALTlem3  24373  blcld  24829  causs  25624  itg2addlem  26084  rplogsum  27859  ltsres  28024  wlkonl1iedg  30249  trlf1  30286  spthdifv  30324  upgrwlkdvde  30328  usgr2pth  30355  pthdlem2  30359  uspgrn2crct  30402  crctcshwlkn0  30415  clwlkclwwlklem2  30596  clwwlknon0  30689  3spthd  30782  ofpreima2  33307  esumpinfval  34751  eulerpartlemf  35048  fin2so  38623  fdc  38772  lshpcmp  40138  lfl1  40220  frege124d  44854  onfrALTlem2  45622  3ornot23VD  45922  ordelordALTVD  45942  onfrALTlem2VD  45964  ndmaovass  48369  elfz2z  48478  lighneallem4  48788