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  4823  csbexg  5265  snopeqop  5466  xpcan2  6150  tfindsg  7837  findsg  7873  ixpexg  8895  fipwss  9380  ranklim  9797  fin23lem14  10286  fzoval  13621  modsumfzodifsn  13909  hashge2el2dif  14445  iswrdi  14482  swrd0  14623  swrdsbslen  14629  swrdspsleq  14630  pfxccatin12  14698  swrdccat  14700  pfxccat3a  14703  repswswrd  14749  cshword  14756  cshwcsh2id  14794  dvdsabseq  16283  m1exp1  16346  flodddiv4  16385  dfgcd2  16516  lcmftp  16606  prmop1  17009  fvprmselelfz  17015  ressbas  17206  resseqnbas  17212  ressinbas  17215  cntzval  19253  symg2bas  19323  sralem  21083  srasca  21087  sravsca  21088  sraip  21089  ocvval  21576  dsmmval  21643  dmatmul  22384  1mavmul  22435  mavmul0g  22440  1marepvmarrepid  22462  smadiadetglem2  22559  1elcpmat  22602  decpmatid  22657  tnglem  24528  tngds  24536  gausslemma2dlem1a  27276  2lgslem1c  27304  2sqreulem1  27357  2sqreunnlem1  27360  nosupno  27615  nosupbday  27617  nosupbnd1lem5  27624  nosupbnd1  27626  nosupbnd2  27628  noinfno  27630  noinfbday  27632  noinfbnd1lem5  27639  noinfbnd1  27641  noinfbnd2  27643  madess  27788  abssge0  28147  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwwisshclwwsn  29945  clwwlknon1nloop  30028  eucrctshift  30172  eucrct2eupth  30174  unopbd  31944  nmopcoi  32024  resvsca  33304  resvlem  33305  satfv1lem  35349  bj-prmoore  37103  ax12indalem  38938  afvres  47173  afvco2  47177  2ffzoeq  47328  difmodm1lt  47360  ply1mulgsumlem2  48376  lcoel0  48417  lindslinindsimp1  48446  digexp  48596  dig1  48597  itsclc0yqsol  48753