MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1rl Structured version   Visualization version   GIF version

Theorem simp1rl 1305
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1rl (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜑)

Proof of Theorem simp1rl
StepHypRef Expression
1 simprl 811 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant1 1128 1 (((𝜒 ∧ (𝜑𝜓)) ∧ 𝜃𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  f1imass  6684  smo11  7630  zsupss  11970  lsmcv  19343  lspsolvlem  19344  mat2pmatghm  20737  mat2pmatmul  20738  plyadd  24172  plymul  24173  coeeu  24180  aannenlem1  24282  logexprlim  25149  ax5seglem6  26013  ax5seg  26017  mdetpmtr1  30198  mdetpmtr2  30199  wsuclem  32076  btwnconn1lem2  32501  btwnconn1lem3  32502  btwnconn1lem4  32503  btwnconn1lem12  32511  lshpsmreu  34899  2llnmat  35313  lvolex3N  35327  lnjatN  35569  pclfinclN  35739  lhpat3  35835  cdlemd6  35993  cdlemfnid  36354  cdlemk19ylem  36720  dihlsscpre  37025  dih1dimb2  37032  dihglblem6  37131  pellex  37901  mullimc  40351  mullimcf  40358  limcperiod  40363  cncfshift  40590  cncfperiod  40595
  Copyright terms: Public domain W3C validator