Theorem pm2.61ian 827

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

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

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 196  df-an 385

This theorem is referenced by:  4cases  987  consensus  990  cases2  1005  sbcrextOLD  3479  csbexg  4720  xpcan2  5490  tfindsg  6952  findsg  6985  ixpexg  7818  fipwss  8218  ranklim  8590  fin23lem14  9038  fzoval  12340  modsumfzodifsn  12605  hashge2el2dif  13117  iswrdi  13164  ffz0iswrd  13187  swrd0  13286  swrdsbslen  13300  swrdspsleq  13301  swrdccatin12  13342  swrdccat  13344  repswswrd  13382  cshword  13388  cshwcsh2id  13425  dvdsabseq  14873  m1exp1  14931  flodddiv4  14975  dfgcd2  15101  lcmftp  15187  prmop1  15580  fvprmselelfz  15586  ressbas  15757  resslem  15760  ressinbas  15763  cntzval  17577  symg2bas  17641  sralem  18998  srasca  19002  sravsca  19003  sraip  19004  ocvval  19830  dsmmval  19897  dmatmul  20122  1mavmul  20173  mavmul0g  20178  1marepvmarrepid  20200  smadiadetglem2  20297  1elcpmat  20339  decpmatid  20394  tnglem  22254  tngds  22262  gausslemma2dlem1a  24890  2lgslem1c  24918  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwwisshclwwn  26336  unopbd  28258  nmopcoi  28338  resvsca  29161  resvlem  29162  ax12indalem  33248  afvres  39901  afvco2  39905  pfxccatin12  40288  pfxccat3a  40292  cshword2  40300  2ffzoeq  40361  uvtxa01vtx  40624  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwwisshclwwsn  41236  eucrctshift  41411  eucrct2eupth  41413  ply1mulgsumlem2  41969  lcoel0  42011  lindslinindsimp1  42040  difmodm1lt  42111  digexp  42199  dig1  42200