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  4053  neldif  4084  reuss2  4275  pssdifn0  4319  dfiun2g  4992  elinxp  6016  ordunidif  6412  eceqoveq  8826  infxpenlem  10020  ackbij1lem18  10242  isf32lem2  10360  ingru  10828  indpi  10920  nqereu  10942  elpq  13029  elfz0ubfz0  13691  elfzmlbp  13698  elfzo0z  13761  fzofzim  13769  fzo1fzo0n0  13775  elfzodifsumelfzo  13791  swrdswrd  14778  swrdccatin1  14798  swrd2lsw  15029  p1modz1  16355  dfgcd2  16642  algcvga  16675  pcprendvds  16938  restntr  23413  filconn  24115  filssufilg  24143  ufileu  24151  ufilen  24162  alexsubALTlem3  24281  blcld  24737  causs  25532  itg2addlem  25992  rplogsum  27771  ltsres  27906  wlkonl1iedg  30131  trlf1  30168  spthdifv  30206  upgrwlkdvde  30210  usgr2pth  30237  pthdlem2  30241  uspgrn2crct  30284  crctcshwlkn0  30297  clwlkclwwlklem2  30478  clwwlknon0  30571  3spthd  30664  ofpreima2  33147  esumpinfval  34591  eulerpartlemf  34889  fin2so  38369  fdc  38503  lshpcmp  39869  lfl1  39951  frege124d  44609  onfrALTlem2  45377  3ornot23VD  45677  ordelordALTVD  45697  onfrALTlem2VD  45719  ndmaovass  48102  elfz2z  48211  lighneallem4  48521