Theorem pm2.61ian 823

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

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

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 210  df-an 401

This theorem is referenced by:  4cases  1054  cases2ALT  1062  consensus  1066  preqsnd  4820  csbexg  5265  snopeqop  5480  xpcan2  6167  tfindsg  7845  findsg  7882  ixpexg  8908  fipwss  9377  ranklim  9804  fin23lem14  10305  fzoval  13679  modsumfzodifsn  13971  hashge2el2dif  14507  iswrdi  14544  swrd0  14686  swrdsbslen  14692  swrdspsleq  14693  pfxccatin12  14760  swrdccat  14762  pfxccat3a  14765  repswswrd  14811  cshword  14818  cshwcsh2id  14855  dvdsabseq  16361  m1exp1  16424  flodddiv4  16463  dfgcd2  16594  lcmftp  16684  prmop1  17088  fvprmselelfz  17094  ressbas  17286  resseqnbas  17292  ressinbas  17295  cntzval  19382  symg2bas  19454  sralem  21266  srasca  21270  sravsca  21271  sraip  21272  ocvval  21777  dsmmval  21844  dmatmul  22615  1mavmul  22666  mavmul0g  22671  1marepvmarrepid  22693  smadiadetglem2  22790  1elcpmat  22833  decpmatid  22888  tnglem  24758  tngds  24766  gausslemma2dlem1a  27487  2lgslem1c  27515  2sqreulem1  27568  2sqreunnlem1  27571  nosupno  27825  nosupbday  27827  nosupbnd1lem5  27834  nosupbnd1  27836  nosupbnd2  27838  noinfno  27840  noinfbday  27842  noinfbnd1lem5  27849  noinfbnd1  27851  noinfbnd2  27853  madess  28017  abssge0  28396  clwlkclwwlklem2a4  30257  clwlkclwwlklem2a  30258  clwwisshclwwsn  30276  clwwlknon1nloop  30359  eucrctshift  30503  eucrct2eupth  30505  unopbd  32276  nmopcoi  32356  resvsca  33567  resvlem  33568  satfv1lem  35725  bj-prmoore  37617  ax12indalem  39581  afvres  47764  afvco2  47768  2ffzoeq  47920  difmodm1lt  47957  ply1mulgsumlem2  49018  lcoel0  49059  lindslinindsimp1  49088  digexp  49238  dig1  49239  itsclc0yqsol  49395