Theorem pm2.61ian 811

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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61ian.2	. . 3 ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)
4	3	ex 412	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜒))
5	2, 4	pm2.61i 182	1 ⊢ (𝜓 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ 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:  4cases  1040  cases2ALT  1048  consensus  1052  preqsnd  4806  csbexg  5243  snopeqop  5441  xpcan2  6119  tfindsg  7786  findsg  7822  ixpexg  8841  fipwss  9308  ranklim  9732  fin23lem14  10219  fzoval  13555  modsumfzodifsn  13846  hashge2el2dif  14382  iswrdi  14419  swrd0  14561  swrdsbslen  14567  swrdspsleq  14568  pfxccatin12  14635  swrdccat  14637  pfxccat3a  14640  repswswrd  14686  cshword  14693  cshwcsh2id  14730  dvdsabseq  16219  m1exp1  16282  flodddiv4  16321  dfgcd2  16452  lcmftp  16542  prmop1  16945  fvprmselelfz  16951  ressbas  17142  resseqnbas  17148  ressinbas  17151  cntzval  19228  symg2bas  19300  sralem  21105  srasca  21109  sravsca  21110  sraip  21111  ocvval  21599  dsmmval  21666  dmatmul  22407  1mavmul  22458  mavmul0g  22463  1marepvmarrepid  22485  smadiadetglem2  22582  1elcpmat  22625  decpmatid  22680  tnglem  24550  tngds  24558  gausslemma2dlem1a  27298  2lgslem1c  27326  2sqreulem1  27379  2sqreunnlem1  27382  nosupno  27637  nosupbday  27639  nosupbnd1lem5  27646  nosupbnd1  27648  nosupbnd2  27650  noinfno  27652  noinfbday  27654  noinfbnd1lem5  27661  noinfbnd1  27663  noinfbnd2  27665  madess  27816  abssge0  28178  clwlkclwwlklem2a4  29969  clwlkclwwlklem2a  29970  clwwisshclwwsn  29988  clwwlknon1nloop  30071  eucrctshift  30215  eucrct2eupth  30217  unopbd  31987  nmopcoi  32067  resvsca  33289  resvlem  33290  satfv1lem  35398  bj-prmoore  37149  ax12indalem  38984  afvres  47203  afvco2  47207  2ffzoeq  47358  difmodm1lt  47390  ply1mulgsumlem2  48419  lcoel0  48460  lindslinindsimp1  48489  digexp  48639  dig1  48640  itsclc0yqsol  48796