Theorem pm2.61ian 848

Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)

Hypotheses

Ref	Expression
pm2.61ian.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
pm2.61ian.2	⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
pm2.61ian	⊢ (𝜓 → 𝜒)

Proof of Theorem pm2.61ian

Step	Hyp	Ref	Expression
1		pm2.61ian.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 403	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61ian.2	. . 3 ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)
4	3	ex 403	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜒))
5	2, 4	pm2.61i 177	1 ⊢ (𝜓 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  4cases  1069  cases2ALT  1077  consensus  1081  preqsnd  4608  csbexg  5018  snopeqop  5192  xpcan2  5813  tfindsg  7322  findsg  7355  ixpexg  8200  fipwss  8605  ranklim  8985  fin23lem14  9471  fzoval  12767  modsumfzodifsn  13039  hashge2el2dif  13552  iswrdi  13579  ffz0iswrd  13602  ccat1st1st  13689  swrd0  13724  swrdsbslen  13739  swrdspsleq  13740  pfxccatin12  13832  swrdccatin12OLD  13833  swrdccat  13836  swrdccatOLD  13837  pfxccat3a  13840  repswswrd  13901  cshword  13911  cshwcsh2id  13950  dvdsabseq  15413  m1exp1  15468  flodddiv4  15511  dfgcd2  15637  lcmftp  15723  prmop1  16114  fvprmselelfz  16120  ressbas  16294  resslem  16297  ressinbas  16300  cntzval  18105  symg2bas  18169  sralem  19539  srasca  19543  sravsca  19544  sraip  19545  ocvval  20375  dsmmval  20442  dmatmul  20672  1mavmul  20723  mavmul0g  20728  1marepvmarrepid  20750  smadiadetglem2  20848  1elcpmat  20891  decpmatid  20946  tnglem  22815  tngds  22823  gausslemma2dlem1a  25504  2lgslem1c  25532  clwlkclwwlklem2a4  27327  clwlkclwwlklem2a  27328  clwwisshclwwsn  27355  clwwlknon1nloop  27474  eucrctshift  27621  eucrct2eupthOLD  27624  eucrct2eupth  27625  unopbd  29430  nmopcoi  29510  resvsca  30376  resvlem  30377  noprefixmo  32388  nosupno  32389  nosupbday  32391  nosupbnd1lem5  32398  nosupbnd1  32400  nosupbnd2  32402  ax12indalem  35021  afvres  42075  afvco2  42079  2ffzoeq  42227  ply1mulgsumlem2  43023  lcoel0  43065  lindslinindsimp1  43094  difmodm1lt  43165  digexp  43249  dig1  43250  itsclc0lem4  43312