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  4065  neldif  4097  reuss2  4289  pssdifn0  4331  dfiun2g  4994  elinxp  5990  ordunidif  6382  eceqoveq  8795  infxpenlem  9966  ackbij1lem18  10189  isf32lem2  10307  ingru  10768  indpi  10860  nqereu  10882  elpq  12934  elfz0ubfz0  13593  elfzmlbp  13600  elfzo0z  13662  fzofzim  13670  fzo1fzo0n0  13676  elfzodifsumelfzo  13692  swrdswrd  14670  swrdccatin1  14690  swrd2lsw  14918  p1modz1  16229  dfgcd2  16516  algcvga  16549  pcprendvds  16811  restntr  23069  filconn  23770  filssufilg  23798  ufileu  23806  ufilen  23817  alexsubALTlem3  23936  blcld  24393  causs  25198  itg2addlem  25659  rplogsum  27438  sltres  27574  wlkonl1iedg  29593  trlf1  29626  spthdifv  29663  upgrwlkdvde  29667  usgr2pth  29694  pthdlem2  29698  uspgrn2crct  29738  crctcshwlkn0  29751  clwlkclwwlklem2  29929  clwwlknon0  30022  3spthd  30105  ofpreima2  32590  esumpinfval  34063  eulerpartlemf  34361  fin2so  37601  fdc  37739  lshpcmp  38981  lfl1  39063  frege124d  43750  onfrALTlem2  44536  3ornot23VD  44836  ordelordALTVD  44856  onfrALTlem2VD  44878  ndmaovass  47207  elfz2z  47316  lighneallem4  47611