Theorem 3simpc 1147

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

Assertion

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

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	3adant1 1127	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  3adantl1  1163  3adantr1  1166  pr1eqbg  4747  fpropnf1  7003  find  7587  findOLD  7588  tz7.49c  8065  eqsup  8904  fimin2g  8945  mulcanenq  10371  elnpi  10399  divcan2  11295  diveq0  11297  divrec  11303  divcan3  11313  eliooord  12784  fzrev3  12968  modaddabs  13272  modaddmod  13273  muladdmodid  13274  modmulmod  13299  sqdiv  13483  swrdlend  14006  swrdnd  14007  ccats1pfxeqbi  14095  sqrmo  14603  muldvds2  15627  dvdscmul  15628  dvdsmulc  15629  dvdstr  15638  funcestrcsetclem9  17390  funcsetcestrclem9  17405  gsumccat  17998  domneq0  20063  znleval2  20247  redvr  20306  aspid  20561  scmatscmiddistr  21113  1marepvmarrepid  21180  mat2pmatghm  21335  pmatcollpw1lem1  21379  monmatcollpw  21384  pmatcollpwscmatlem2  21395  conncompss  22038  islly2  22089  elmptrab2  22433  tngngp3  23262  lmmcvg  23865  cmslsschl  23981  ivthicc  24062  aaliou3lem7  24945  logimcl  25161  qrngdiv  26208  ax5seg  26732  uhgr2edg  26998  umgr2edgneu  27004  uspgr1ewop  27038  iswlkg  27403  wlkonwlk  27452  trlontrl  27500  upgrwlkdvspth  27528  pthonpth  27537  spthonpthon  27540  uhgrwkspth  27544  usgr2wlkspthlem1  27546  usgr2wlkspthlem2  27547  usgr2wlkspth  27548  2pthon3v  27729  umgr2wlk  27735  rusgrnumwwlkg  27762  clwwisshclwws  27800  clwwlknp  27822  clwwlkfo  27835  clwwlknwwlkncl  27838  1pthond  27929  uhgr3cyclex  27967  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  numclwwlk3  28170  ajfuni  28642  funadj  29669  fovcld  30399  trleile  30679  isinftm  30860  bnj1098  32165  bnj546  32278  bnj998  32339  bnj1006  32342  bnj1173  32384  bnj1189  32391  cusgr3cyclex  32496  elnanelprv  32789  cgr3permute1  33622  cgr3com  33627  brifs2  33652  idinside  33658  btwnconn1  33675  lineunray  33721  wl-nfeqfb  34941  riotasv2s  36254  lsatlspsn2  36288  3dim2  36764  paddasslem14  37129  4atexlemex6  37370  cdlemg10bALTN  37932  cdlemg44  38029  tendoplcl  38077  hdmap14lem14  39177  pm13.194  41116  fmulcl  42223  fmuldfeqlem1  42224  stoweidlem17  42659  stoweidlem31  42673  dfsalgen2  42981  sigaraf  43467  sigarmf  43468  elfzelfzlble  43878  funcringcsetcALTV2lem9  44668  funcringcsetclem9ALTV  44691  zlmodzxzscm  44759  divsub1dir  44926  elbigoimp  44970  digexp  45021  2arymptfv  45064