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  4835  csbexg  5280  snopeqop  5481  xpcan2  6166  tfindsg  7856  findsg  7893  ixpexg  8936  fipwss  9441  ranklim  9858  fin23lem14  10347  fzoval  13677  modsumfzodifsn  13962  hashge2el2dif  14498  iswrdi  14535  swrd0  14676  swrdsbslen  14682  swrdspsleq  14683  pfxccatin12  14751  swrdccat  14753  pfxccat3a  14756  repswswrd  14802  cshword  14809  cshwcsh2id  14847  dvdsabseq  16332  m1exp1  16395  flodddiv4  16434  dfgcd2  16565  lcmftp  16655  prmop1  17058  fvprmselelfz  17064  ressbas  17257  resseqnbas  17263  ressinbas  17266  cntzval  19304  symg2bas  19374  sralem  21134  srasca  21138  sravsca  21139  sraip  21140  ocvval  21627  dsmmval  21694  dmatmul  22435  1mavmul  22486  mavmul0g  22491  1marepvmarrepid  22513  smadiadetglem2  22610  1elcpmat  22653  decpmatid  22708  tnglem  24579  tngds  24587  gausslemma2dlem1a  27328  2lgslem1c  27356  2sqreulem1  27409  2sqreunnlem1  27412  nosupno  27667  nosupbday  27669  nosupbnd1lem5  27676  nosupbnd1  27678  nosupbnd2  27680  noinfno  27682  noinfbday  27684  noinfbnd1lem5  27691  noinfbnd1  27693  noinfbnd2  27695  madess  27840  abssge0  28199  clwlkclwwlklem2a4  29978  clwlkclwwlklem2a  29979  clwwisshclwwsn  29997  clwwlknon1nloop  30080  eucrctshift  30224  eucrct2eupth  30226  unopbd  31996  nmopcoi  32076  resvsca  33348  resvlem  33349  satfv1lem  35384  bj-prmoore  37133  ax12indalem  38963  afvres  47201  afvco2  47205  2ffzoeq  47356  ply1mulgsumlem2  48363  lcoel0  48404  lindslinindsimp1  48433  difmodm1lt  48502  digexp  48587  dig1  48588  itsclc0yqsol  48744