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  4032  neldif  4073  reuss2  4274  pssdifn0  4319  dfiun2g  4991  elinxp  6020  ordunidif  6431  eceqoveq  8871  infxpenlem  10119  ackbij1lem18  10341  isf32lem2  10459  ingru  10927  indpi  11019  nqereu  11041  elpq  13130  elfz0ubfz0  13793  elfzmlbp  13800  elfzo0z  13863  fzofzim  13871  fzo1fzo0n0  13877  elfzodifsumelfzo  13893  swrdswrd  14882  swrdccatin1  14902  swrd2lsw  15134  p1modz1  16458  dfgcd2  16748  algcvga  16783  pcprendvds  17047  restntr  23530  filconn  24232  filssufilg  24260  ufileu  24268  ufilen  24279  alexsubALTlem3  24398  blcld  24854  causs  25649  itg2addlem  26109  rplogsum  27884  ltsres  28049  wlkonl1iedg  30274  trlf1  30311  spthdifv  30349  upgrwlkdvde  30353  usgr2pth  30380  pthdlem2  30384  uspgrn2crct  30427  crctcshwlkn0  30440  clwlkclwwlklem2  30621  clwwlknon0  30714  3spthd  30807  ofpreima2  33332  esumpinfval  34775  eulerpartlemf  35072  fin2so  38722  fdc  38871  lshpcmp  40237  lfl1  40319  frege124d  44953  onfrALTlem2  45720  3ornot23VD  46020  ordelordALTVD  46040  onfrALTlem2VD  46062  ndmaovass  48481  elfz2z  48590  lighneallem4  48900