Theorem 3simpc 1053

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Assertion

Ref	Expression
3simpc	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		3anrot 1036	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
2		3simpa 1051	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒))
3	1, 2	sylbi 206	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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  df-3an 1033

This theorem is referenced by:  simp3  1056  3adant1  1072  3adantl1  1210  3adantr1  1213  find  6983  tz7.49c  7428  eqsup  8245  fimin2g  8286  mulcanenq  9661  elnpi  9689  divcan2  10572  diveq0  10574  divrec  10580  divcan3  10590  eliooord  12104  fzrev3  12276  modaddabs  12570  modaddmod  12571  muladdmodid  12572  modmulmod  12597  sqdiv  12790  swrdlend  13283  swrdnd  13284  ccats1swrdeqbi  13349  sqrmo  13840  muldvds2  14845  dvdscmul  14846  dvdsmulc  14847  dvdstr  14856  funcestrcsetclem9  16611  funcsetcestrclem9  16626  domneq0  19118  aspid  19151  znleval2  19723  redvr  19782  scmatscmiddistr  20133  1marepvmarrepid  20200  mat2pmatghm  20354  pmatcollpw1lem1  20398  monmatcollpw  20403  pmatcollpwscmatlem2  20414  concompss  21046  islly2  21097  elmptrab2OLD  21441  elmptrab2  21442  tngngp3  22270  lmmcvg  22867  ivthicc  23034  aaliou3lem7  23908  logimcl  24120  qrngdiv  25113  ax5seg  25618  usgra2edg1  25912  constr2trl  26129  constr3trllem2  26179  constr3pthlem2  26184  clwwlkfo  26325  clwwlknwwlkncl  26328  clwwisshclww  26335  clwlkfclwwlk  26371  clwlkf1clwwlklem  26376  rusgranumwlkg  26485  numclwwlkovgelim  26616  numclwwlk3  26636  ajfuni  27099  funadj  28129  fovcld  28820  trleile  28997  isinftm  29066  bnj1098  30108  bnj546  30220  bnj998  30280  bnj1006  30283  bnj1173  30324  bnj1189  30331  cgr3permute1  31325  cgr3com  31330  brifs2  31355  idinside  31361  btwnconn1  31378  lineunray  31424  wl-nfeqfb  32502  riotasv2s  33262  lsatlspsn2  33297  3dim2  33772  paddasslem14  34137  4atexlemex6  34378  cdlemg10bALTN  34942  cdlemg44  35039  tendoplcl  35087  hdmap14lem14  36191  pm13.194  37635  fmulcl  38648  fmuldfeqlem1  38649  stoweidlem17  38910  stoweidlem31  38924  dfsalgen2  39235  sigaraf  39691  sigarmf  39692  ccats1pfxeqbi  40294  pr1eqbg  40313  fpropnf1  40337  elfzelfzlble  40358  uhgr2edg  40435  umgr2edgneu  40441  uspgr1ewop  40474  is1wlkg  40816  upgrwlkedg  40850  wlkOnprop  40866  wlkOnwlk  40870  trlsonprop  40915  trlOntrl  40918  upgrwlkdvde  40943  upgrwlkdvspth  40945  pthsonprop  40950  spthonprop  40951  pthOnpth  40954  spthonpthon  40957  uhgr1wlkspth  40961  usgr2wlkneq  40962  usgr2wlkspthlem1  40963  usgr2wlkspthlem2  40964  usgr2wlkspth  40965  usgr2pth  40970  2pthon3v-av  41150  umgr2wlk  41156  rusgrnumwwlkg  41179  clwwlksfo  41225  clwwlksnwwlkncl  41228  clwwisshclwws  41235  clwlksfclwwlk  41269  clwlksf1clwwlklem  41275  1pthond  41311  uhgr3cyclex  41349  av-numclwlk1lem2f1  41524  av-numclwlk2lem2f  41533  av-numclwwlk3  41539  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  zlmodzxzscm  41928  divsub1dir  42101  elbigoimp  42148  digexp  42199