Theorem pm2.61ian 824

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ 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:  4cases  1056  cases2ALT  1064  consensus  1068  preqsnd  4826  csbexg  5275  snopeqop  5491  xpcan2  6177  tfindsg  7859  findsg  7896  ixpexg  8922  fipwss  9392  ranklim  9819  fin23lem14  10328  fzoval  13700  modsumfzodifsn  13993  hashge2el2dif  14530  iswrdi  14567  swrd0  14713  swrdsbslen  14719  swrdspsleq  14720  pfxccatin12  14787  swrdccat  14789  pfxccat3a  14792  repswswrd  14840  cshword  14847  cshwcsh2id  14884  dvdsabseq  16388  m1exp1  16451  flodddiv4  16490  dfgcd2  16621  lcmftp  16711  prmop1  17115  fvprmselelfz  17121  ressbas  17313  resseqnbas  17319  ressinbas  17322  cntzval  19414  symg2bas  19486  sralem  21326  srasca  21330  sravsca  21331  sraip  21332  isfieldidl  21415  ocvval  21846  dsmmval  21913  dmatmul  22683  1mavmul  22734  mavmul0g  22739  1marepvmarrepid  22761  smadiadetglem2  22858  1elcpmat  22901  decpmatid  22956  tnglem  24826  tngds  24834  gausslemma2dlem1a  27558  2lgslem1c  27586  2sqreulem1  27639  2sqreunnlem1  27642  nosupno  27896  nosupbday  27898  nosupbnd1lem5  27905  nosupbnd1  27907  nosupbnd2  27909  noinfno  27911  noinfbday  27913  noinfbnd1lem5  27920  noinfbnd1  27922  noinfbnd2  27924  madess  28088  abssge0  28467  clwlkclwwlklem2a4  30377  clwlkclwwlklem2a  30378  clwwisshclwwsn  30396  clwwlknon1nloop  30479  eucrctshift  30623  eucrct2eupth  30625  unopbd  32396  nmopcoi  32476  resvsca  33675  resvlem  33676  satfv1lem  35867  bj-prmoore  37790  ax12indalem  39752  afvres  47942  afvco2  47946  2ffzoeq  48098  difmodm1lt  48135  ply1mulgsumlem2  49200  lcoel0  49241  lindslinindsimp1  49270  digexp  49420  dig1  49421  itsclc0yqsol  49577