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  4825  csbexg  5272  snopeqop  5487  xpcan2  6174  tfindsg  7853  findsg  7890  ixpexg  8916  fipwss  9385  ranklim  9812  fin23lem14  10313  fzoval  13684  modsumfzodifsn  13976  hashge2el2dif  14513  iswrdi  14550  swrd0  14692  swrdsbslen  14698  swrdspsleq  14699  pfxccatin12  14766  swrdccat  14768  pfxccat3a  14771  repswswrd  14817  cshword  14824  cshwcsh2id  14861  dvdsabseq  16367  m1exp1  16430  flodddiv4  16469  dfgcd2  16600  lcmftp  16690  prmop1  17094  fvprmselelfz  17100  ressbas  17292  resseqnbas  17298  ressinbas  17301  cntzval  19387  symg2bas  19459  sralem  21271  srasca  21275  sravsca  21276  sraip  21277  ocvval  21782  dsmmval  21849  dmatmul  22619  1mavmul  22670  mavmul0g  22675  1marepvmarrepid  22697  smadiadetglem2  22794  1elcpmat  22837  decpmatid  22892  tnglem  24762  tngds  24770  gausslemma2dlem1a  27491  2lgslem1c  27519  2sqreulem1  27572  2sqreunnlem1  27575  nosupno  27829  nosupbday  27831  nosupbnd1lem5  27838  nosupbnd1  27840  nosupbnd2  27842  noinfno  27844  noinfbday  27846  noinfbnd1lem5  27853  noinfbnd1  27855  noinfbnd2  27857  madess  28021  abssge0  28400  clwlkclwwlklem2a4  30285  clwlkclwwlklem2a  30286  clwwisshclwwsn  30304  clwwlknon1nloop  30387  eucrctshift  30531  eucrct2eupth  30533  unopbd  32304  nmopcoi  32384  resvsca  33591  resvlem  33592  satfv1lem  35749  bj-prmoore  37640  ax12indalem  39604  afvres  47791  afvco2  47795  2ffzoeq  47947  difmodm1lt  47984  ply1mulgsumlem2  49045  lcoel0  49086  lindslinindsimp1  49115  digexp  49265  dig1  49266  itsclc0yqsol  49422