Theorem pm2.61ian 817

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

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

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 208  df-an 397

This theorem is referenced by:  4cases  1046  cases2ALT  1054  consensus  1058  preqsnd  4790  csbexg  5232  snopeqop  5447  xpcan2  6128  tfindsg  7801  findsg  7837  ixpexg  8860  fipwss  9332  ranklim  9759  fin23lem14  10246  fzoval  13605  modsumfzodifsn  13897  hashge2el2dif  14433  iswrdi  14470  swrd0  14612  swrdsbslen  14618  swrdspsleq  14619  pfxccatin12  14686  swrdccat  14688  pfxccat3a  14691  repswswrd  14737  cshword  14744  cshwcsh2id  14781  dvdsabseq  16273  m1exp1  16336  flodddiv4  16375  dfgcd2  16506  lcmftp  16596  prmop1  17000  fvprmselelfz  17006  ressbas  17197  resseqnbas  17203  ressinbas  17206  cntzval  19287  symg2bas  19359  sralem  21166  srasca  21170  sravsca  21171  sraip  21172  ocvval  21642  dsmmval  21709  dmatmul  22480  1mavmul  22531  mavmul0g  22536  1marepvmarrepid  22558  smadiadetglem2  22655  1elcpmat  22698  decpmatid  22753  tnglem  24623  tngds  24631  gausslemma2dlem1a  27346  2lgslem1c  27374  2sqreulem1  27427  2sqreunnlem1  27430  nosupno  27685  nosupbday  27687  nosupbnd1lem5  27694  nosupbnd1  27696  nosupbnd2  27698  noinfno  27700  noinfbday  27702  noinfbnd1lem5  27709  noinfbnd1  27711  noinfbnd2  27713  madess  27876  abssge0  28255  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwwisshclwwsn  30104  clwwlknon1nloop  30187  eucrctshift  30331  eucrct2eupth  30333  unopbd  32104  nmopcoi  32184  resvsca  33415  resvlem  33416  satfv1lem  35590  bj-prmoore  37473  ax12indalem  39437  afvres  47635  afvco2  47639  2ffzoeq  47791  difmodm1lt  47828  ply1mulgsumlem2  48878  lcoel0  48919  lindslinindsimp1  48948  digexp  49098  dig1  49099  itsclc0yqsol  49255