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  4111  neldif  4143  reuss2  4331  pssdifn0  4373  dfiun2g  5034  elinxp  6038  ordunidif  6434  eceqoveq  8860  infxpenlem  10050  ackbij1lem18  10273  isf32lem2  10391  ingru  10852  indpi  10944  nqereu  10966  elpq  13014  elfz0ubfz0  13668  elfzmlbp  13675  elfzo0z  13737  fzofzim  13745  fzo1fzo0n0  13750  elfzodifsumelfzo  13766  swrdswrd  14739  swrdccatin1  14759  swrd2lsw  14987  p1modz1  16293  dfgcd2  16579  algcvga  16612  pcprendvds  16873  restntr  23205  filconn  23906  filssufilg  23934  ufileu  23942  ufilen  23953  alexsubALTlem3  24072  blcld  24533  causs  25345  itg2addlem  25807  rplogsum  27585  sltres  27721  wlkonl1iedg  29697  trlf1  29730  spthdifv  29765  upgrwlkdvde  29769  usgr2pth  29796  pthdlem2  29800  uspgrn2crct  29837  crctcshwlkn0  29850  clwlkclwwlklem2  30028  clwwlknon0  30121  3spthd  30204  ofpreima2  32682  esumpinfval  34053  eulerpartlemf  34351  fin2so  37593  fdc  37731  lshpcmp  38969  lfl1  39051  frege124d  43750  onfrALTlem2  44543  3ornot23VD  44844  ordelordALTVD  44864  onfrALTlem2VD  44886  ndmaovass  47155  elfz2z  47264  lighneallem4  47534